# HG changeset patch
# User paulson
# Date 880562146 -3600
# Node ID 9abce31cc7646422190dac85922462fa6cb757ae
# Parent  0727c8d8a35975f0ff3e652c94824add3b0f3ddf
Added rule impCE'

diff -r 0727c8d8a359 -r 9abce31cc764 src/FOL/FOL.ML
--- a/src/FOL/FOL.ML	Wed Nov 26 17:35:08 1997 +0100
+++ b/src/FOL/FOL.ML	Wed Nov 26 17:35:46 1997 +0100
@@ -53,6 +53,15 @@
   [ (resolve_tac [excluded_middle RS disjE] 1),
     (DEPTH_SOLVE (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)) ]);
+
 (*Double negation law*)
 qed_goal "notnotD" FOL.thy "~~P ==> P"
  (fn [major]=>