1.1 --- a/NEWS	Wed Aug 17 17:02:16 2005 +0200
     1.2 +++ b/NEWS	Wed Aug 17 17:03:20 2005 +0200
     1.3 @@ -155,6 +155,9 @@
     1.4  rather than 'types'.  INCOMPATIBILITY for new object-logic
     1.5  specifications.
     1.6  
     1.7 +* Attributes 'induct' and 'cases': type or set names may now be
     1.8 +locally fixed variables as well.
     1.9 +
    1.10  * Simplifier: can now control the depth to which conditional rewriting
    1.11  is traced via the PG menu Isabelle -> Settings -> Trace Simp Depth
    1.12  Limit.
    1.13 @@ -186,21 +189,33 @@
    1.14  
    1.15  
    1.16  *** Locales ***
    1.17 -  
    1.18 -* New commands for the interpretation of locale expressions in
    1.19 -theories ('interpretation') and proof contexts ('interpret').  These
    1.20 -take an instantiation of the locale parameters and compute proof
    1.21 -obligations from the instantiated specification.  After the
    1.22 -obligations have been discharged, the instantiated theorems of the
    1.23 -locale are added to the theory or proof context.  Interpretation is
    1.24 -smart in that already active interpretations do not occur in proof
    1.25 -obligations, neither are instantiated theorems stored in duplicate.
    1.26 -Use print_interps to inspect active interpretations of a particular
    1.27 -locale.  For details, see the Isar Reference manual.
    1.28 +
    1.29 +* New commands for the interpretation of locale expressions in theories (1),
    1.30 +locales (2) and proof contexts (3).  These generate proof obligations from
    1.31 +the expression specification.  After the obligations have been discharged,
    1.32 +theorems of the expression are added to the theory, target locale or proof
    1.33 +context.  The synopsis of the commands is a follows:
    1.34 +  (1) interpretation expr inst
    1.35 +  (2) interpretation target < expr
    1.36 +  (3) interpret expr inst
    1.37 +Interpretation in theories and proof contexts require a parameter
    1.38 +instantiation of terms from the current context.  This is applied to
    1.39 +specifications and theorems of the interpreted expression.  Interpretation
    1.40 +in locales only permits parameter renaming through the locale expression.
    1.41 +Interpretation is smart in that interpretation that are active already
    1.42 +do not occur in proof obligations, neither are instantiated theorems stored
    1.43 +in duplicate.  Use 'print_interps' to inspect active interpretations of
    1.44 +a particular locale.  For details, see the Isar Reference manual.
    1.45  
    1.46  INCOMPATIBILITY: former 'instantiate' has been withdrawn, use
    1.47  'interpret' instead.
    1.48  
    1.49 +* New context element 'constrains' for adding type constraints to parameters.
    1.50 +
    1.51 +* Context expressions: renaming of parameters with syntax redeclaration.
    1.52 +
    1.53 +* Locale declaration: 'includes' disallowed.
    1.54 +
    1.55  * Proper static binding of attribute syntax -- i.e. types / terms /
    1.56  facts mentioned as arguments are always those of the locale definition
    1.57  context, independently of the context of later invocations.  Moreover,
    1.58 @@ -218,22 +233,11 @@
    1.59  on the context and the facts involved -- may have to assign parsed
    1.60  values to argument tokens explicitly.
    1.61  
    1.62 -* New context element "constrains" adds type constraints to parameters --
    1.63 -there is no logical significance.
    1.64 -
    1.65 -* Context expressions: renaming parameters permits syntax
    1.66 -redeclaration as well.
    1.67 -
    1.68 -* Locale definition: 'includes' now disallowed.
    1.69 -
    1.70  * Changed parameter management in theorem generation for long goal
    1.71  statements with 'includes'.  INCOMPATIBILITY: produces a different
    1.72  theorem statement in rare situations.
    1.73  
    1.74 -* Attributes 'induct' and 'cases': type or set names may now be
    1.75 -locally fixed variables as well.
    1.76 -
    1.77 -* Antiquotations now provide the option 'locale=NAME' to specify an
    1.78 +* Antiquotations provide the option 'locale=NAME' to specify an
    1.79  alternative context used for evaluating and printing the subsequent
    1.80  argument, as in @{thm [locale=LC] fold_commute}, for example.
    1.81