# HG changeset patch
# User nipkow
# Date 832776856 -7200
# Node ID 978ee7ededdd897b5b0412130eb4c5e1543a479a
# Parent  17001ecd546ede0ab207ce3ea6447b4bf19b7938
Added swap_prems_rl

diff -r 17001ecd546e -r 978ee7ededdd src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue May 21 13:42:53 1996 +0200
+++ b/src/Pure/drule.ML	Wed May 22 16:54:16 1996 +0200
@@ -57,6 +57,7 @@
   val RLN		: thm list * (int * thm list) -> thm list
   val size_of_thm	: thm -> int
   val standard		: thm -> thm
+  val swap_prems_rl     : thm
   val symmetric_thm	: thm
   val thin_rl		: thm
   val transitive_thm	: thm
@@ -632,6 +633,23 @@
                            (implies_intr V  (forall_intr x (assume V))))
   end;
 
+(* (PROP ?PhiA ==> PROP ?PhiB ==> PROP ?Psi) ==>
+   (PROP ?PhiB ==> PROP ?PhiA ==> PROP ?Psi)
+   `thm COMP swap_prems_rl' swaps the first two premises of `thm'
+*)
+val swap_prems_rl =
+  let val cmajor = read_cterm Sign.proto_pure
+            ("PROP PhiA ==> PROP PhiB ==> PROP Psi", propT);
+      val major = assume cmajor;
+      val cminor1 = read_cterm Sign.proto_pure  ("PROP PhiA", propT);
+      val minor1 = assume cminor1;
+      val cminor2 = read_cterm Sign.proto_pure  ("PROP PhiB", propT);
+      val minor2 = assume cminor2;
+  in standard
+       (implies_intr cmajor (implies_intr cminor2 (implies_intr cminor1
+         (implies_elim (implies_elim major minor1) minor2))))
+  end;
+
 end;
 
 open Drule;