# HG changeset patch
# User wenzelm
# Date 1113053737 -7200
# Node ID 406a98ee802750de95a1f9707fe03411009ed383
# Parent  64f76b974a8d1aa3084753d9516ca932502cf9b2
update syntax of 'where' and 'of';

diff -r 64f76b974a8d -r 406a98ee8027 doc-src/IsarRef/pure.tex
--- 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}