# HG changeset patch
# User lcp
# Date 788176345 -3600
# Node ID 650ee089809b0208e9962c4ac26db66f3ed205b1
# Parent  11e4827b3d75251ba97334df27d9e623688c0fca
Added Krzysztof's theorem disj_imp_disj

diff -r 11e4827b3d75 -r 650ee089809b src/FOL/IFOL.ML
--- a/src/FOL/IFOL.ML	Wed Dec 21 13:36:02 1994 +0100
+++ b/src/FOL/IFOL.ML	Fri Dec 23 10:52:25 1994 +0100
@@ -358,3 +358,9 @@
     "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
  (fn major::prems=>
   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
+
+(*Courtesy Krzysztof Grabczewski*)
+val major::prems = goal IFOL.thy "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
+br (major RS disjE) 1;
+by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
+qed "disj_imp_disj";