changeset 13518 | a0749ce05100 |
parent 13500 | 2222c7a0e8bb |
child 13522 | 934fffeb6f38 |
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