--- 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;
--- 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
--- 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 *)