--- 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 ***