added case_tac to be like HOL
authorpaulson
Fri Jul 17 11:24:09 1998 +0200 (1998-07-17)
changeset 51598fc4fb20d70f
parent 5158 48ca9ef35fb0
child 5160 1ff6679144b9
added case_tac to be like HOL
src/FOL/FOL.ML
     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