src/Doc/IsarRef/Proof.thy
changeset 55143 04448228381d
parent 55112 b1a5d603fd12
child 55837 154855d9a564
     1.1 --- a/src/Doc/IsarRef/Proof.thy	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/Doc/IsarRef/Proof.thy	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -721,11 +721,13 @@
     1.4      ;
     1.5      @@{attribute OF} @{syntax thmrefs}
     1.6      ;
     1.7 -    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})?
     1.8 +    @@{attribute of} @{syntax insts} ('concl' ':' @{syntax insts})? \<newline>
     1.9 +      (@'for' (@{syntax vars} + @'and'))?
    1.10      ;
    1.11      @@{attribute "where"}
    1.12        ((@{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}) '='
    1.13 -      (@{syntax type} | @{syntax term}) * @'and')
    1.14 +      (@{syntax type} | @{syntax term}) * @'and') \<newline>
    1.15 +      (@'for' (@{syntax vars} + @'and'))?
    1.16    \<close>}
    1.17  
    1.18    \begin{description}
    1.19 @@ -812,6 +814,10 @@
    1.20    left to right; ``@{text _}'' (underscore) indicates to skip a
    1.21    position.  Arguments following a ``@{text "concl:"}'' specification
    1.22    refer to positions of the conclusion of a rule.
    1.23 +
    1.24 +  An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
    1.25 +  be specified: the instantiated theorem is exported, and these
    1.26 +  variables become schematic (usually with some shifting of indices).
    1.27    
    1.28    \item @{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots> x\<^sub>n = t\<^sub>n"}
    1.29    performs named instantiation of schematic type and term variables
    1.30 @@ -821,6 +827,9 @@
    1.31    As type instantiations are inferred from term instantiations,
    1.32    explicit type instantiations are seldom necessary.
    1.33  
    1.34 +  An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
    1.35 +  be specified as for @{attribute "of"} above.
    1.36 +
    1.37    \end{description}
    1.38  *}
    1.39