*** empty log message ***
authornipkow
Fri, 23 Aug 2002 11:08:01 +0200
changeset 13518 a0749ce05100
parent 13517 42efec18f5b2
child 13519 36ee816b5ee3
*** empty log message ***
NEWS
--- a/NEWS	Fri Aug 23 07:41:05 2002 +0200
+++ b/NEWS	Fri Aug 23 11:08:01 2002 +0200
@@ -55,6 +55,9 @@
 * simp's arithmetic capabilities have been enhanced a bit: it now
 takes ~= in premises into account (by performing a case split);
 
+* simp reduces "m*(n div m) + n mod m" to n, even if the two summands are
+  distributed over a sum of terms.
+
 
 *** ML ***