NEWS
changeset 14175 dbd16ebaf907
parent 14173 a3690aeb79d4
child 14199 d3b8d972a488
     1.1 --- a/NEWS	Fri Aug 29 15:19:02 2003 +0200
     1.2 +++ b/NEWS	Fri Aug 29 15:40:11 2003 +0200
     1.3 @@ -17,6 +17,22 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
    1.10 +
    1.11 +  - Now understand static (Isar) contexts.  As a consequence, users of Isar
    1.12 +    locales are no longer forced to write Isar proof scripts.
    1.13 +    For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    1.14 +    emulations.
    1.15 +  - INCOMPATIBILITY: names of variables to be instantiated may no
    1.16 +    longer be enclosed in quotes.  Instead, precede variable names containing
    1.17 +    dots with `?'.  This is consistent with the instantiation attribute
    1.18 +    "where".
    1.19 +
    1.20 +* HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.21 +  (Isar) contexts.
    1.22 +
    1.23  *** HOL ***
    1.24  
    1.25  * 'specification' command added, allowing for definition by