# HG changeset patch
# User ballarin
# Date 1071062870 -3600
# Node ID 92ed032e83a1f4babe49aa54d7faf450874275f4
# Parent  f1abe67c448ab51c91677c02525b397489068a0a
Isar: where attribute supports instantiation of type vars.

diff -r f1abe67c448a -r 92ed032e83a1 NEWS
--- a/NEWS	Sun Dec 07 16:30:06 2003 +0100
+++ b/NEWS	Wed Dec 10 14:27:50 2003 +0100
@@ -42,9 +42,10 @@
     This is consistent with the instantiation attribute "where".
 
 * Attributes "where" and "of":
-  Now take type variables of instantiated theorem into account when reading
-  the instantiation string.  This fixes a bug that caused instantiated
-  theorems to have too special types in some circumstances.
+  - Now take type variables of instantiated theorem into account when reading
+    the instantiation string.  This fixes a bug that caused instantiated
+    theorems to have too special types in some circumstances.
+  - "where" permits explicit instantiations of type variables.
 
 * Calculation commands "moreover" and "also":
   Do not reset facts ("this") any more.
diff -r f1abe67c448a -r 92ed032e83a1 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Sun Dec 07 16:30:06 2003 +0100
+++ b/doc-src/IsarRef/pure.tex	Wed Dec 10 14:27:50 2003 +0100
@@ -1055,17 +1055,21 @@
   \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.  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
-  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.
+\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.
 
 \end{descr}