src/FOL/IFOL.ML
changeset 821 650ee089809b
parent 793 0b5c5f568d74
child 1002 280ec187f8e1
equal deleted inserted replaced
820:11e4827b3d75 821:650ee089809b
   356 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   356 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   357 qed_goal "ex_impE" IFOL.thy 
   357 qed_goal "ex_impE" IFOL.thy 
   358     "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
   358     "[| (EX x.P(x))-->S;  P(x)-->S ==> R |] ==> R"
   359  (fn major::prems=>
   359  (fn major::prems=>
   360   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
   360   [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]);
       
   361 
       
   362 (*Courtesy Krzysztof Grabczewski*)
       
   363 val major::prems = goal IFOL.thy "[| P|Q;  P==>R;  Q==>S |] ==> R|S";
       
   364 br (major RS disjE) 1;
       
   365 by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));
       
   366 qed "disj_imp_disj";