--- a/NEWS Wed Sep 06 10:01:27 2006 +0200
+++ b/NEWS Wed Sep 06 13:48:02 2006 +0200
@@ -465,6 +465,20 @@
*** 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:
+
+ - new constants Numeral.pred and Numeral.succ instead
+ of former Numeral.bin_pred and Numeral.bin_succ.
+ - Use integer operations instead of bin_add, bin_mult and so on.
+ - Numeral simplification theorems named Numeral.numeral_simps instead of Bin_simps.
+ - ML structure Bin_Simprocs now named Int_Numeral_Base_Simprocs.
+
+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