# HG changeset patch # User haftmann # Date 1193672782 -3600 # Node ID 59afe8a0a7e1173d8e3dccb590d6355dfd5a1e95 # Parent bf72a258b57b4f9f1fdb4ebf14156178ca5746ca added nbe diff -r bf72a258b57b -r 59afe8a0a7e1 ANNOUNCE --- 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.