1.1 --- a/src/FOL/FOL.ML	Fri Jul 17 11:23:17 1998 +0200
     1.2 +++ b/src/FOL/FOL.ML	Fri Jul 17 11:24:09 1998 +0200
     1.3 @@ -43,6 +43,14 @@
     1.4  fun excluded_middle_tac sP =
     1.5      res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
     1.6  
     1.7 +qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
     1.8 +  (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
     1.9 +                  etac p2 1, etac p1 1]);
    1.10 +
    1.11 +(*HOL's more natural case analysis tactic*)
    1.12 +fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
    1.13 +
    1.14 +
    1.15  (*** Special elimination rules *)
    1.16  
    1.17