doc-src/IsarRef/pure.tex
 changeset 14285 92ed032e83a1 parent 14212 cd05b503ca2d child 14642 2bfe5de2d1fa
     1.1 --- a/doc-src/IsarRef/pure.tex	Sun Dec 07 16:30:06 2003 +0100
1.2 +++ b/doc-src/IsarRef/pure.tex	Wed Dec 10 14:27:50 2003 +0100
1.3 @@ -1055,17 +1055,21 @@
1.4    \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
1.5    effectively skipped by including $\_$'' (underscore) as argument.
1.6
1.7 -\item [$of~\vec t$] performs positional instantiation.  The terms $\vec t$ are
1.8 -  substituted for any schematic variables occurring in a theorem from left to
1.9 -  right; \texttt{_}'' (underscore) indicates to skip a position.  Arguments
1.10 -  following a $concl\colon$'' specification refer to positions of the
1.11 -  conclusion of a rule.
1.12 +\item [$of~\vec t$] performs positional instantiation of term
1.13 +  variables.  The terms $\vec t$ are substituted for any schematic
1.14 +  variables occurring in a theorem from left to right; \texttt{_}''
1.15 +  (underscore) indicates to skip a position.  Arguments following a
1.16 +  $concl\colon$'' specification refer to positions of the conclusion
1.17 +  of a rule.
1.18
1.19 -\item [$where~\vec x = \vec t$] performs named instantiation of schematic
1.20 -  variables occurring in a theorem.  Schematic variables
1.21 -  have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The
1.22 -  question mark may be omitted if the variable name is neither a
1.23 -  keyword nor contains a dot.
1.24 +\item [$where~\vec x = \vec t$] performs named instantiation of
1.25 +  schematic type and term variables occurring in a theorem.  Schematic
1.26 +  variables have to be specified on the left-hand side (e.g.\
1.27 +  $?x1\!.\!3$).  The question mark may be omitted if the variable name
1.28 +  is neither a keyword nor contains a dot.  Types are instantiated
1.29 +  before terms, and instantiations have to be written in that order.
1.30 +  Because type instantiations are inferred from term instantiations,
1.31 +  explicit type instantiations are seldom necessary.
1.32
1.33  \end{descr}
1.34