--- a/src/Pure/drule.ML Wed Feb 15 21:35:00 2006 +0100
+++ b/src/Pure/drule.ML Wed Feb 15 21:35:02 2006 +0100
@@ -75,6 +75,7 @@
val revcut_rl: thm
val thin_rl: thm
val triv_forall_equality: thm
+ val distinct_prems_rl: thm
val swap_prems_rl: thm
val equal_intr_rule: thm
val equal_elim_rule1: thm
@@ -772,6 +773,18 @@
(implies_intr V (forall_intr x (assume V))))
end;
+(* (PROP ?Phi ==> PROP ?Phi ==> PROP ?Psi) ==>
+ (PROP ?Phi ==> PROP ?Psi)
+*)
+val distinct_prems_rl =
+ let
+ val AAB = read_prop "PROP Phi ==> PROP Phi ==> PROP Psi"
+ val A = read_prop "PROP Phi";
+ in
+ store_standard_thm_open "distinct_prems_rl"
+ (implies_intr_list [AAB, A] (implies_elim_list (assume AAB) [assume A, assume A]))
+ 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'