doc-src/Ref/thm.tex
changeset 9288 06a55195741b
parent 9258 2121ff73a37d
child 9499 7e6988210488
--- a/doc-src/Ref/thm.tex	Wed Jul 12 14:47:55 2000 +0200
+++ b/doc-src/Ref/thm.tex	Wed Jul 12 16:44:34 2000 +0200
@@ -76,6 +76,7 @@
 RSN : thm * (int * thm) -> thm                 \hfill\textbf{infix}
 RS  : thm * thm -> thm                         \hfill\textbf{infix}
 MRS : thm list * thm -> thm                    \hfill\textbf{infix}
+OF  : thm * thm list -> thm                    \hfill\textbf{infix}
 RLN : thm list * (int * thm list) -> thm list  \hfill\textbf{infix}
 RL  : thm list * thm list -> thm list          \hfill\textbf{infix}
 MRL : thm list list * thm list -> thm list     \hfill\textbf{infix}
@@ -100,6 +101,10 @@
   premises of $thm$.  Because the theorems are used from right to left, it
   does not matter if the $thm@i$ create new premises.  {\tt MRS} is useful
   for expressing proof trees.
+  
+\item[\tt {$thm$ OF $[thm@1,\ldots,thm@n]$}] \indexbold{*OF} is the same as
+  \texttt{$[thm@1,\ldots,thm@n]$ MRS $thm$}, with slightly more readable
+  argument order, though.
 
 \item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN} 
   joins lists of theorems.  For every $thm@1$ in $thms@1$ and $thm@2$ in