changeset 5159 | 8fc4fb20d70f |
parent 4308 | 9abce31cc764 |
child 7355 | 4c43090659ca |
--- a/src/FOL/FOL.ML Fri Jul 17 11:23:17 1998 +0200 +++ b/src/FOL/FOL.ML Fri Jul 17 11:24:09 1998 +0200 @@ -43,6 +43,14 @@ fun excluded_middle_tac sP = res_inst_tac [("Q",sP)] (excluded_middle RS disjE); +qed_goal "case_split_thm" FOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q" + (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, + etac p2 1, etac p1 1]); + +(*HOL's more natural case analysis tactic*) +fun case_tac a = res_inst_tac [("P",a)] case_split_thm; + + (*** Special elimination rules *)