added nbe

--- 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.