author | lcp |
Thu, 11 May 1995 10:42:19 +0200 | |
changeset 1119 | 49ed9a415637 |
parent 1118 | 93ba05d8ccdc |
child 1120 | ff7dd80513e6 |
--- a/doc-src/Ref/thm.tex Thu May 11 10:38:30 1995 +0200 +++ b/doc-src/Ref/thm.tex Thu May 11 10:42:19 1995 +0200 @@ -595,7 +595,7 @@ \[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \] -\item[\tt $thm@1$ COMP $thm@2$] +\item[$thm@1$ \ttindexbold{COMP} $thm@2$] calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if unique; otherwise, it raises exception~\xdx{THM}\@. It is analogous to {\tt RS}\@.