# HG changeset patch
# User nipkow
# Date 1150388912 -7200
# Node ID cab56c9493508de6b08e65acc59376780f172eff
# Parent  7c7e15b271454a02312bf2c4eac69ab24a4db75d
*** empty log message ***

diff -r 7c7e15b27145 -r cab56c949350 NEWS
--- a/NEWS	Thu Jun 15 17:50:47 2006 +0200
+++ b/NEWS	Thu Jun 15 18:28:32 2006 +0200
@@ -389,6 +389,13 @@
 
 *** HOL ***
 
+* New top level command 'normal_form' computes the normal form of a term
+that may contain free variables. For example 'normal_form "rev[a,b,c]"'
+prints '[b,c,a]'. This command is suitable for heavy-duty computations
+because the functions are compiled to ML first.
+INCOMPATIBILITY: new keywords 'normal_form' must quoted when used as
+an identifier.
+
 * Alternative iff syntax "A <-> B" for equality on bool (with priority
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).