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