# HG changeset patch
# User wenzelm
# Date 1140035702 -3600
# Node ID 5212516f1a98374e945e95a09a88da8d5bb85753
# Parent  527bc006f2b6888e30df441f0b91b41b351503d1
added distinct_prems_rl;

diff -r 527bc006f2b6 -r 5212516f1a98 src/Pure/drule.ML
--- 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'