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";