# HG changeset patch
# User ballarin
# Date 1254422986 -7200
# Node ID 29941e925c82f6b7d1b1b5909cc68084a63e7378
# Parent  d2d0b9b1a69dc7754ad66e7b4dbe0882c5dabaa8
News entry: inheritance of mixins; print_interps.

diff -r d2d0b9b1a69d -r 29941e925c82 NEWS
--- 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 ***