NEWS
changeset 14551 2cb6ff394bfb
parent 14547 e0c0179100c9
child 14556 c5078f6c99a9
     1.1 --- a/NEWS	Tue Apr 13 07:48:32 2004 +0200
     1.2 +++ b/NEWS	Tue Apr 13 09:42:40 2004 +0200
     1.3 @@ -85,13 +85,17 @@
     1.4    - Rule sets <locale>.intro and <locale>.axioms no longer declared as
     1.5      [intro?] and [elim?] (respectively) by default.
     1.6    - Experimental command for instantiation of locales in proof contexts:
     1.7 -        instantiate <label>: <loc>
     1.8 +        instantiate <label>[<attrs>]: <loc>
     1.9      Instantiates locale <loc> and adds all its theorems to the current context
    1.10 -    taking into account their attributes, and qualifying their names with
    1.11 -    <label>.  If the locale has assumptions, a chained fact of the form
    1.12 +    taking into account their attributes.  Label and attrs are optional
    1.13 +    modifiers, like in theorem declarations.  If present, names of
    1.14 +    instantiated theorems are qualified with <label>, and the attributes
    1.15 +    <attrs> are applied after any attributes these theorems might have already.
    1.16 +      If the locale has assumptions, a chained fact of the form
    1.17      "<loc> t1 ... tn" is expected from which instantiations of the parameters
    1.18 -    are derived.
    1.19 -    A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
    1.20 +    are derived.  The command does not support old-style locales declared
    1.21 +    with "locale (open)".
    1.22 +      A few (very simple) examples can be found in FOL/ex/LocaleInst.thy.
    1.23  
    1.24  * HOL: Tactic emulation methods induct_tac and case_tac understand static
    1.25    (Isar) contexts.