diff -r e567f3425267 -r b0acd74da01d NEWS
--- a/NEWS	Mon Dec 01 18:22:38 1997 +0100
+++ b/NEWS	Mon Dec 01 18:27:06 1997 +0100
@@ -117,6 +117,12 @@
 
 * HOL/Map: new theory of `maps' a la VDM;
 
+* HOL/simplifier: simplification procedures nat_cancel_sums for
+cancelling out common nat summands from =, <, <= (in)equalities, or
+differences; simplification procedures nat_cancel_factor for
+cancelling common factor from =, <, <= (in)equalities over natural
+sums;  nat_cancel contains both kinds of procedures;
+
 * HOL/simplifier: terms of the form
   `? x. P1(x) & ... & Pn(x) & x=t & Q1(x) & ... Qn(x)'  (or t=x)
   are rewritten to