# HG changeset patch
# User paulson
# Date 957797873 -7200
# Node ID bcceda950cd01a6fb385d71dc6f8e6515ce25abe
# Parent  b824c0c55613da8f56c1267f6bcb40b90bd04fc1
more details

diff -r b824c0c55613 -r bcceda950cd0 NEWS
--- a/NEWS	Mon May 08 11:45:57 2000 +0200
+++ b/NEWS	Mon May 08 16:57:53 2000 +0200
@@ -115,9 +115,13 @@
 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.
+* greatly improved simplification involving numerals of type nat & int, 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;
+   i*j + k + j*#3*i     simplifies to  #4*(i*j) + k
+  two terms #m*u and #n*u are replaced by #(m+n)*u
+    (where #m, #n and u can implicitly be 1; this is simproc combine_numerals)
+  and the term/formula #m*u+x ~~ #n*u+y simplifies simplifies to #(m-n)+x ~~ y
+    or x ~~ #(n-m)+y, where ~~ is one of = < <= or - (simproc cancel_numerals);
 
 * new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer