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.