NEWS
changeset 9647 e9623f47275b
parent 9612 e6ba17cd012e
child 9701 533df6cedc2d
     1.1 --- a/NEWS	Fri Aug 18 12:30:41 2000 +0200
     1.2 +++ b/NEWS	Fri Aug 18 12:31:20 2000 +0200
     1.3 @@ -303,6 +303,7 @@
     1.4  * the integer library now contains many of the usual laws for the orderings, 
     1.5  including $<=, and monotonicity laws for $+ and $*; 
     1.6  
     1.7 +* new example ZF/ex/NatSum to demonstrate integer arithmetic simplification;
     1.8  
     1.9  *** FOL & ZF ***
    1.10