# HG changeset patch
# User paulson
# Date 948189610 -3600
# Node ID ad1c4a67819671a0bfa8eedf0405942d0a27ba55
# Parent  ceedd1a8bad6aec76b561320dc59739c43a7b3f2
Documented Thm.instantiate (not normalizing) and Drule.instantiate
(normalizing)

diff -r ceedd1a8bad6 -r ad1c4a678196 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Mon Jan 17 15:56:58 2000 +0100
+++ b/doc-src/Ref/thm.tex	Tue Jan 18 11:00:10 2000 +0100
@@ -604,24 +604,32 @@
 applies {\tt forall_elim_var} repeatedly, for every element of the list~$ks$.
 \end{ttdescription}
 
+
 \subsection{Instantiation of unknowns}
 \index{instantiation}
 \begin{ttbox} 
 instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
 \end{ttbox}
+There are two versions of this rule.  The primitive one is
+\ttindexbold{Thm.instantiate}, which merely performs the instantiation and can
+produce a conclusion not in normal form.  A derived version is  
+\ttindexbold{Drule.instantiate}, which normalizes its conclusion.
+
 \begin{ttdescription}
 \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$] 
 simultaneously substitutes types for type unknowns (the
 $tyinsts$) and terms for term unknowns (the $insts$).  Instantiations are
 given as $(v,t)$ pairs, where $v$ is an unknown and $t$ is a term (of the
 same type as $v$) or a type (of the same sort as~$v$).  All the unknowns
-must be distinct.  The rule normalizes its conclusion.
+must be distinct.  
 
-Note that \ttindex{instantiate'} (see \S\ref{sec:instantiate})
+In some cases, \ttindex{instantiate'} (see \S\ref{sec:instantiate})
 provides a more convenient interface to this rule.
 \end{ttdescription}
 
 
+
+
 \subsection{Freezing/thawing type unknowns}
 \index{type unknowns!freezing/thawing of}
 \begin{ttbox}