ANNOUNCE
changeset 25242 6c3890cbceac
parent 25229 2673709fb8f7
child 25259 8d6b03eef9c9
equal deleted inserted replaced
25241:001ab1d3f567 25242:6c3890cbceac
    35 * Various improvements in locale infrastructure (interpretation etc.)
    35 * Various improvements in locale infrastructure (interpretation etc.)
    36 
    36 
    37 * Various improvements of Isar language elements and related proof
    37 * Various improvements of Isar language elements and related proof
    38 tools.
    38 tools.
    39 
    39 
    40 * Second generation code-generator for a subset of HOL, targeting SML,
    40 * Second generation code generator for a subset of HOL, targeting SML,
    41 Haskell, and OCaml.
    41 Haskell, and OCaml.
    42 
    42 
    43 * Command 'normal_form' and method 'normalization'
    43 * Command 'normal_form' and method 'normalization'
    44 for evaluating terms with free variables.
    44 for evaluating terms with free variables.
    45 
    45