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