# HG changeset patch
# User paulson
# Date 957436158 -7200
# Node ID 518a5450ab6d62a06c526b1c6d072405274ed749
# Parent  9aeca9a34cf4175ef6fbfe6b84e25e26a8f34606
simprocs

diff -r 9aeca9a34cf4 -r 518a5450ab6d NEWS
--- a/NEWS	Thu May 04 12:29:00 2000 +0200
+++ b/NEWS	Thu May 04 12:29:18 2000 +0200
@@ -7,6 +7,11 @@
 
 *** Overview of INCOMPATIBILITIES (see below for more details) ***
 
+* HOL: simplification of natural numbers is much changed.  To partly recover
+       the old behaviour (e.g. to prevent n+n rewriting to #2*n) type
+		Delsimprocs Nat_Numeral_Simprocs.cancel_numerals;
+		Delsimprocs [Nat_Numeral_Simprocs.combine_numerals];
+
 * HOL: the constant for f``x is now "image" rather than "op ``";
 
 * HOL: the cartesian product is now "<*>" instead of "Times"; the
@@ -110,8 +115,9 @@
 basically a generalized version of de-Bruijn representation; very
 useful in avoiding lifting all operations;
 
-* greatly improved simplification involving numerals of type "nat", e.g. in
-   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k;
+* greatly improved simplification involving numerals of type "nat", e.g.
+   (i + #8 + j) = Suc k simplifies to  #7 + (i + j) = k
+   i*j + k + j*#3*i     simplifies to  #4*(i*j) + k;
 
 * new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer