diff -r aa3b82085e07 -r e9623f47275b NEWS
--- 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 ***