diff -r f3cafd2929d5 -r dbd16ebaf907 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Aug 29 15:40:11 2003 +0200
@@ -963,7 +963,7 @@
 \indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
 \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
 \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
-\indexisaratt{OF}\indexisaratt{of}
+\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
 \begin{matharray}{rcl}
   - & : & \isarmeth \\
   assumption & : & \isarmeth \\
@@ -976,6 +976,7 @@
   rule & : & \isaratt \\[0.5ex]
   OF & : & \isaratt \\
   of & : & \isaratt \\
+  where & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
@@ -993,6 +994,8 @@
   ;
   'of' insts ('concl' ':' insts)?
   ;
+  'where' (name '=' term * 'and')
+  ;
 \end{rail}
 
 \begin{descr}
@@ -1058,6 +1061,11 @@
   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
+  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 does not contain a dot.
+
 \end{descr}