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