NEWS

--- a/NEWS	Thu Jan 06 17:51:56 2011 +0100
+++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
@@ -498,6 +498,14 @@
 INCOMPATIBILITY.
 
 
+*** HOL-Algebra ***
+
+* Theorems for additive ring operations (locale abelian_monoid and
+descendants) are generated by interpretation from their multiplicative
+counterparts.  This causes slight differences in the simp and clasets.
+INCOMPATIBILITY.
+
+
 *** HOLCF ***
 
 * The domain package now runs in definitional mode by default: The