Documented Thm.instantiate (not normalizing) and Drule.instantiate
Tue, 18 Jan 2000 11:00:10 +0100
changeset 8135 ad1c4a678196
parent 8134 ceedd1a8bad6
child 8136 8c65f3ca13f2
Documented Thm.instantiate (not normalizing) and Drule.instantiate (normalizing)
--- 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$.
 \subsection{Instantiation of unknowns}
 instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
+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.
 \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.
 \subsection{Freezing/thawing type unknowns}
 \index{type unknowns!freezing/thawing of}