src/FOL/FOL.ML
changeset 4308 9abce31cc764
parent 4186 e39f28f94cf8
child 5159 8fc4fb20d70f
     1.1 --- a/src/FOL/FOL.ML	Wed Nov 26 17:35:08 1997 +0100
     1.2 +++ b/src/FOL/FOL.ML	Wed Nov 26 17:35:46 1997 +0100
     1.3 @@ -53,6 +53,15 @@
     1.4    [ (resolve_tac [excluded_middle RS disjE] 1),
     1.5      (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
     1.6  
     1.7 +(*This version of --> elimination works on Q before P.  It works best for
     1.8 +  those cases in which P holds "almost everywhere".  Can't install as
     1.9 +  default: would break old proofs.*)
    1.10 +qed_goal "impCE'" thy 
    1.11 +    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
    1.12 + (fn major::prems=>
    1.13 +  [ (resolve_tac [excluded_middle RS disjE] 1),
    1.14 +    (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
    1.15 +
    1.16  (*Double negation law*)
    1.17  qed_goal "notnotD" FOL.thy "~~P ==> P"
    1.18   (fn [major]=>