diff -r 1b8ff770f02c -r 710cdb9e0d17 NEWS
--- a/NEWS	Thu Jan 06 21:06:17 2011 +0100
+++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
@@ -123,6 +123,11 @@
 * Document antiquotation @{file} checks file/directory entries within
 the local file system.
 
+* Locale interpretation commands 'interpret' and 'sublocale' accept
+equations to map definitions in a locale to appropriate entities in
+the context of the interpretation.  The 'interpretation' command
+already provided this functionality.
+
 
 *** HOL ***
 
@@ -502,8 +507,12 @@
 
 * 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.
+counterparts.  Names (in particular theorem names) have the mandatory
+qualifier 'add'.  Previous theorem names are redeclared for
+compatibility.
+
+* Structure 'int_ring' is now an abbreviation (previously a
+definition).  This fits more natural with advanced interpretations.
 
 
 *** HOLCF ***