equal
deleted
inserted
replaced
420 |
420 |
421 qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q" |
421 qed_goal "case_split_thm" (the_context ()) "[| P ==> Q; ~P ==> Q |] ==> Q" |
422 (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, |
422 (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1, |
423 etac p2 1, etac p1 1]); |
423 etac p2 1, etac p1 1]); |
424 |
424 |
|
425 bind_thm ("case_split", case_split_thm); |
|
426 |
425 fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
427 fun case_tac a = res_inst_tac [("P",a)] case_split_thm; |
426 |
428 |
427 |
429 |
428 (** Standard abbreviations **) |
430 (** Standard abbreviations **) |
429 |
431 |