# HG changeset patch
# User wenzelm
# Date 963413074 -7200
# Node ID 06a55195741bd546c04c7be9de8fc9c96d6f185d
# Parent  c406d0af93683b56c461f1d2ade0edd962765fbf
infix 'OF' is a version of 'MRS' with more appropriate argument order;

diff -r c406d0af9368 -r 06a55195741b NEWS
--- a/NEWS	Wed Jul 12 14:47:55 2000 +0200
+++ b/NEWS	Wed Jul 12 16:44:34 2000 +0200
@@ -230,6 +230,9 @@
 
 * provide TAGS file for Isabelle sources;
 
+* ML: infix 'OF' is a version of 'MRS' with more appropriate argument
+order;
+
 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global
 timing flag supersedes proof_timing and Toplevel.trace;
 
diff -r c406d0af9368 -r 06a55195741b doc-src/Ref/thm.tex
--- 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
diff -r c406d0af9368 -r 06a55195741b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jul 12 14:47:55 2000 +0200
+++ b/src/Pure/drule.ML	Wed Jul 12 16:44:34 2000 +0200
@@ -6,7 +6,7 @@
 Derived rules and other operations on theorems.
 *)
 
-infix 0 RS RSN RL RLN MRS MRL COMP;
+infix 0 RS RSN RL RLN MRS MRL OF COMP;
 
 signature BASIC_DRULE =
 sig
@@ -42,6 +42,7 @@
   val RL                : thm list * thm list -> thm list
   val MRS               : thm list * thm -> thm
   val MRL               : thm list list * thm list -> thm list
+  val OF                : thm * thm list -> thm
   val compose           : thm * int * thm -> thm list
   val COMP              : thm * thm -> thm
   val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm
@@ -349,6 +350,9 @@
         | rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
   in  rs_aux 1 rlss  end;
 
+(*A version of MRS with more appropriate argument order*)
+fun bottom_rl OF rls = rls MRS bottom_rl;
+
 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)