--- a/NEWS Mon Sep 11 12:27:36 2006 +0200
+++ b/NEWS Mon Sep 11 14:28:47 2006 +0200
@@ -466,8 +466,8 @@
*** HOL ***
* Numeral syntax: type 'bin' which was a mere type copy of 'int' has been
-abandoned in favour of plain 'int'. Significant changes for setting up numeral
-syntax for types:
+abandoned in favour of plain 'int'. INCOMPATIBILITY -- Significant changes
+for setting up numeral syntax for types:
- new constants Numeral.pred and Numeral.succ instead
of former Numeral.bin_pred and Numeral.bin_succ.
@@ -477,8 +477,6 @@
See HOL/Integ/IntArith.thy for an example setup.
-INCOMPATIBILITY.
-
* 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