NEWS

--- a/NEWS	Sat Sep 15 20:13:25 2012 +0200
+++ b/NEWS	Sat Sep 15 20:14:29 2012 +0200
@@ -47,6 +47,9 @@
 
 *** HOL ***
 
+* Class "comm_monoid_diff" formalised properties of bounded
+subtraction, with natural numbers and multisets as typical instances.
+
 * Theory "Library/Option_ord" provides instantiation of option type
 to lattice type classes.