1.1 --- a/NEWS	Fri Sep 26 11:08:18 2003 +0200
     1.2 +++ b/NEWS	Tue Sep 30 15:07:38 2003 +0200
     1.3 @@ -20,15 +20,21 @@
     1.4  *** Isar ***
     1.5  
     1.6  * Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
     1.7 -
     1.8    - Now understand static (Isar) contexts.  As a consequence, users of Isar
     1.9      locales are no longer forced to write Isar proof scripts.
    1.10      For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    1.11      emulations.
    1.12    - INCOMPATIBILITY: names of variables to be instantiated may no
    1.13 -    longer be enclosed in quotes.  Instead, precede variable names containing
    1.14 -    dots with `?'.  This is consistent with the instantiation attribute
    1.15 -    "where".
    1.16 +    longer be enclosed in quotes.  Instead, precede variable name with `?'.
    1.17 +    This is consistent with the instantiation attribute "where".
    1.18 +
    1.19 +* Locales:
    1.20 +  - Goal statements involving the context element "includes" no longer
    1.21 +    generate theorems with internal delta predicates (those ending on
    1.22 +    "_axioms") in the premise.
    1.23 +    Resolve particular premise with <locale>.intro to obtain old form.
    1.24 +  - Fixed bug in type inference ("unify_frozen") that prevented mix of target
    1.25 +    specification and "includes" elements in goal statement.
    1.26  
    1.27  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.28    (Isar) contexts.