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