Interpretation in locales.

--- a/NEWS	Wed Aug 17 17:02:16 2005 +0200
+++ b/NEWS	Wed Aug 17 17:03:20 2005 +0200
@@ -155,6 +155,9 @@
 rather than 'types'.  INCOMPATIBILITY for new object-logic
 specifications.
 
+* Attributes 'induct' and 'cases': type or set names may now be
+locally fixed variables as well.
+
 * Simplifier: can now control the depth to which conditional rewriting
 is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
 Limit.
@@ -186,21 +189,33 @@
 
 
 *** Locales ***
-  
-* New commands for the interpretation of locale expressions in
-theories ('interpretation') and proof contexts ('interpret').  These
-take an instantiation of the locale parameters and compute proof
-obligations from the instantiated specification.  After the
-obligations have been discharged, the instantiated theorems of the
-locale are added to the theory or proof context.  Interpretation is
-smart in that already active interpretations do not occur in proof
-obligations, neither are instantiated theorems stored in duplicate.
-Use print_interps to inspect active interpretations of a particular
-locale.  For details, see the Isar Reference manual.
+
+* New commands for the interpretation of locale expressions in theories (1),
+locales (2) and proof contexts (3).  These generate proof obligations from
+the expression specification.  After the obligations have been discharged,
+theorems of the expression are added to the theory, target locale or proof
+context.  The synopsis of the commands is a follows:
+  (1) interpretation expr inst
+  (2) interpretation target < expr
+  (3) interpret expr inst
+Interpretation in theories and proof contexts require a parameter
+instantiation of terms from the current context.  This is applied to
+specifications and theorems of the interpreted expression.  Interpretation
+in locales only permits parameter renaming through the locale expression.
+Interpretation is smart in that interpretation that are active already
+do not occur in proof obligations, neither are instantiated theorems stored
+in duplicate.  Use 'print_interps' to inspect active interpretations of
+a particular locale.  For details, see the Isar Reference manual.
 
 INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
 'interpret' instead.
 
+* New context element 'constrains' for adding type constraints to parameters.
+
+* Context expressions: renaming of parameters with syntax redeclaration.
+
+* Locale declaration: 'includes' disallowed.
+
 * Proper static binding of attribute syntax -- i.e. types / terms /
 facts mentioned as arguments are always those of the locale definition
 context, independently of the context of later invocations.  Moreover,
@@ -218,22 +233,11 @@
 on the context and the facts involved -- may have to assign parsed
 values to argument tokens explicitly.
 
-* New context element "constrains" adds type constraints to parameters --
-there is no logical significance.
-
-* Context expressions: renaming parameters permits syntax
-redeclaration as well.
-
-* Locale definition: 'includes' now disallowed.
-
 * Changed parameter management in theorem generation for long goal
 statements with 'includes'.  INCOMPATIBILITY: produces a different
 theorem statement in rare situations.
 
-* Attributes 'induct' and 'cases': type or set names may now be
-locally fixed variables as well.
-
-* Antiquotations now provide the option 'locale=NAME' to specify an
+* Antiquotations provide the option 'locale=NAME' to specify an
 alternative context used for evaluating and printing the subsequent
 argument, as in @{thm [locale=LC] fold_commute}, for example.