# HG changeset patch
# User paulson
# Date 880561398 -3600
# Node ID 2c99775d953fe7edebdecca5e4cd692ffb7d4331
# Parent  ed343192de45c76dd96d6027612ca695ff4a87bf
Added rule impCE'

diff -r ed343192de45 -r 2c99775d953f src/HOL/HOL.ML
--- a/src/HOL/HOL.ML	Wed Nov 26 17:16:48 1997 +0100
+++ b/src/HOL/HOL.ML	Wed Nov 26 17:23:18 1997 +0100
@@ -321,6 +321,15 @@
   [ rtac (excluded_middle RS disjE) 1,
     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
 
+(*This version of --> elimination works on Q before P.  It works best for
+  those cases in which P holds "almost everywhere".  Can't install as
+  default: would break old proofs.*)
+qed_goal "impCE'" thy 
+    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
+ (fn major::prems=>
+  [ (resolve_tac [excluded_middle RS disjE] 1),
+    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
+
 (*Classical <-> elimination. *)
 qed_goal "iffCE" HOL.thy
     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"