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