NEWS
changeset 14508 859b11514537
parent 14503 255ad604e08e
child 14536 43e436a4f293
     1.1 --- a/NEWS	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/NEWS	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -52,7 +52,8 @@
     1.4  
     1.5  *** Isar ***
     1.6  
     1.7 -* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
     1.8 +* Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
     1.9 +  cut_tac, subgoal_tac and thin_tac:
    1.10    - Now understand static (Isar) contexts.  As a consequence, users of Isar
    1.11      locales are no longer forced to write Isar proof scripts.
    1.12      For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
    1.13 @@ -79,6 +80,14 @@
    1.14      specification and "includes" elements in goal statement.
    1.15    - Rule sets <locale>.intro and <locale>.axioms no longer declared as
    1.16      [intro?] and [elim?] (respectively) by default.
    1.17 +  - Experimental command for instantiation of locales in proof contexts:
    1.18 +        instantiate <label>: <loc>
    1.19 +    Instantiates locale <loc> and adds all its theorems to the current context
    1.20 +    taking into account their attributes, and qualifying their names with
    1.21 +    <label>.  If the locale has assumptions, a chained fact of the form
    1.22 +    "<loc> t1 ... tn" is expected from which instantiations of the parameters
    1.23 +    are derived.
    1.24 +    A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
    1.25  
    1.26  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.27    (Isar) contexts.