changeset 18531 | ce7b80b7c84e |
parent 18522 | 9bdfb6eaf8ab |
child 18591 | 04b9f2bf5a48 |
--- a/src/HOL/HOL.thy Sat Dec 31 21:49:38 2005 +0100 +++ b/src/HOL/HOL.thy Sat Dec 31 21:49:39 2005 +0100 @@ -909,15 +909,6 @@ subsubsection {* Classical Reasoner setup *} -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 hypsubst_setup