equal
deleted
inserted
replaced
728 shows "Q" |
728 shows "Q" |
729 apply (rule excluded_middle [THEN disjE]) |
729 apply (rule excluded_middle [THEN disjE]) |
730 apply (erule prem2) |
730 apply (erule prem2) |
731 apply (erule prem1) |
731 apply (erule prem1) |
732 done |
732 done |
733 |
|
734 ML {* |
|
735 fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split} |
|
736 *} |
|
737 |
733 |
738 (*Classical implies (-->) elimination. *) |
734 (*Classical implies (-->) elimination. *) |
739 lemma impCE: |
735 lemma impCE: |
740 assumes major: "P-->Q" |
736 assumes major: "P-->Q" |
741 and minor: "~P ==> R" "Q ==> R" |
737 and minor: "~P ==> R" "Q ==> R" |