ANNOUNCE
changeset 25228 59afe8a0a7e1
parent 25213 48a1e80f5cdb
child 25229 2673709fb8f7
     1.1 --- a/ANNOUNCE	Mon Oct 29 16:13:47 2007 +0100
     1.2 +++ b/ANNOUNCE	Mon Oct 29 16:46:22 2007 +0100
     1.3 @@ -40,6 +40,9 @@
     1.4  * Second generation code-generator for a subset of HOL, targeting SML,
     1.5  Haskell, and OCaml.
     1.6  
     1.7 +* Command 'normal_form' and method 'normalization'
     1.8 +for evaluating terms with free variables.
     1.9 +
    1.10  * Improved support for arbitrary ML operations depending on the
    1.11  logical context.
    1.12