NEWS

--- a/NEWS	Fri Mar 30 10:41:27 2012 +0200
+++ b/NEWS	Fri Mar 30 11:16:35 2012 +0200
@@ -162,6 +162,9 @@
   mod_mult_distrib ~> mult_mod_left
   mod_mult_distrib2 ~> mult_mod_right
 
+* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
+generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
+
 * More default pred/set conversions on a couple of relation operations
 and predicates.  Added powers of predicate relations.
 Consolidation of some relation theorems: