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