--- a/NEWS Thu Oct 01 20:37:33 2009 +0200
+++ b/NEWS Thu Oct 01 20:49:46 2009 +0200
@@ -15,6 +15,14 @@
* On instantiation of classes, remaining undefined class parameters
are formally declared. INCOMPATIBILITY.
+* Locale interpretation propagates mixins along the locale hierarchy.
+The currently only available mixins are the equations used to map
+local definitions to terms of the target domain of an interpretation.
+
+* Reactivated diagnositc command 'print_interps'. Use 'print_interps l'
+to print all interpretations of locale l in the theory. Interpretations
+in proofs are not shown.
+
*** HOL ***