doc-src/Ref/thm.tex
changeset 3135 233aba197bf2
parent 3108 335efc3f5632
child 3485 f27a30a18a17
--- a/doc-src/Ref/thm.tex	Wed May 07 17:21:04 1997 +0200
+++ b/doc-src/Ref/thm.tex	Wed May 07 17:21:24 1997 +0200
@@ -557,7 +557,7 @@
 \subsection{Instantiation of unknowns}
 \index{instantiation}
 \begin{ttbox} 
-instantiate: (indexname * ctyp) list * (cterm * cterm) list -> thm -> thm
+instantiate: (indexname * ctyp){\thinspace}list * (cterm * cterm){\thinspace}list -> thm -> thm
 \end{ttbox}
 \begin{ttdescription}
 \item[\ttindexbold{instantiate} ($tyinsts$, $insts$) $thm$]