changeset 18522 | 9bdfb6eaf8ab |
parent 18511 | beed2bc052a3 |
child 18531 | ce7b80b7c84e |
--- a/src/FOL/FOL.thy Fri Dec 30 16:56:54 2005 +0100 +++ b/src/FOL/FOL.thy Fri Dec 30 16:56:56 2005 +0100 @@ -24,6 +24,15 @@ use "FOL_lemmas1.ML" theorems case_split = case_split_thm [case_names True False, cases type: o] +lemma cla_dist_concl: + assumes x: "~Z_Z ==> PROP X_X" + and z: "PROP Y_Y ==> Z_Z" + and y: "PROP X_X ==> PROP Y_Y" + shows Z_Z + apply (rule classical) + apply (erule x [THEN y, THEN z]) + done + use "cladata.ML" setup Cla.setup setup cla_setup