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$]