--- a/NEWS Thu Sep 25 09:28:07 2008 +0200
+++ b/NEWS Thu Sep 25 09:28:08 2008 +0200
@@ -66,7 +66,10 @@
*** HOL ***
-* HOL/Main: command "value" now integrates different evaluation
+* Normalization by evaluation now allows non-leftlinear equations.
+Declare with attribute [code nbe].
+
+* Command "value" now integrates different evaluation
mechanisms. The result of the first successful evaluation mechanism
is printed. In square brackets a particular named evaluation
mechanisms may be specified (currently, [SML], [code] or [nbe]). See