NEWS
changeset 4335 b0acd74da01d
parent 4325 e72cba5af6c5
child 4357 b852e2d2a39a
     1.1 --- a/NEWS	Mon Dec 01 18:22:38 1997 +0100
     1.2 +++ b/NEWS	Mon Dec 01 18:27:06 1997 +0100
     1.3 @@ -117,6 +117,12 @@
     1.4  
     1.5  * HOL/Map: new theory of `maps' a la VDM;
     1.6  
     1.7 +* HOL/simplifier: simplification procedures nat_cancel_sums for
     1.8 +cancelling out common nat summands from =, <, <= (in)equalities, or
     1.9 +differences; simplification procedures nat_cancel_factor for
    1.10 +cancelling common factor from =, <, <= (in)equalities over natural
    1.11 +sums;  nat_cancel contains both kinds of procedures;
    1.12 +
    1.13  * HOL/simplifier: terms of the form
    1.14    `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
    1.15    are rewritten to