ANNOUNCE
changeset 25228 59afe8a0a7e1
parent 25213 48a1e80f5cdb
child 25229 2673709fb8f7
equal deleted inserted replaced
25227:bf72a258b57b 25228:59afe8a0a7e1
    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'
       
    44 for evaluating terms with free variables.
       
    45 
    43 * Improved support for arbitrary ML operations depending on the
    46 * Improved support for arbitrary ML operations depending on the
    44 logical context.
    47 logical context.
    45 
    48 
    46 * Parallel loading of theories based on native multicore support in
    49 * Parallel loading of theories based on native multicore support in
    47 Poly/ML 5.1.
    50 Poly/ML 5.1.