author | nipkow |
Fri, 23 Aug 2002 11:08:01 +0200 | |
changeset 13518 | a0749ce05100 |
parent 13517 | 42efec18f5b2 |
child 13519 | 36ee816b5ee3 |
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