--- a/doc-src/IsarRef/pure.tex Sat Apr 09 15:34:38 2005 +0200
+++ b/doc-src/IsarRef/pure.tex Sat Apr 09 15:35:37 2005 +0200
@@ -1038,7 +1038,7 @@
;
'of' insts ('concl' ':' insts)?
;
- 'where' (name '=' term * 'and')
+ 'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
;
\end{rail}
@@ -1099,21 +1099,18 @@
\cite[\S5]{isabelle-ref}, but note the reversed order. Positions may be
effectively skipped by including ``$\_$'' (underscore) as argument.
-\item [$of~\vec t$] performs positional instantiation of term
- variables. The terms $\vec t$ are substituted for any schematic
- variables occurring in a theorem from left to right; ``\texttt{_}''
- (underscore) indicates to skip a position. Arguments following a
- ``$concl\colon$'' specification refer to positions of the conclusion
- of a rule.
+\item [$of~\vec t$] performs positional instantiation of term variables. The
+ terms $\vec t$ are substituted for any schematic variables occurring in a
+ theorem from left to right; ``\texttt{_}'' (underscore) indicates to skip a
+ position. Arguments following a ``$concl\colon$'' specification refer to
+ positions of the conclusion of a rule.
-\item [$where~\vec x = \vec t$] performs named instantiation of
- schematic type and term variables occurring in a theorem. Schematic
- variables have to be specified on the left-hand side (e.g.\
- $?x1\!.\!3$). The question mark may be omitted if the variable name
- is neither a keyword nor contains a dot. Types are instantiated
- before terms, and instantiations have to be written in that order.
- Because type instantiations are inferred from term instantiations,
- explicit type instantiations are seldom necessary.
+\item [$where~\vec x = \vec t$] performs named instantiation of schematic type
+ and term variables occurring in a theorem. Schematic variables have to be
+ specified on the left-hand side (e.g.\ $?x1\!.\!3$). The question mark may
+ be omitted if the variable name is a plain identifier without index. As
+ type instantiations are inferred from term instantiations, explicit type
+ instantiations are seldom necessary.
\end{descr}