src/FOL/FOL.thy

--- a/src/FOL/FOL.thy	Sat Dec 31 21:49:38 2005 +0100
+++ b/src/FOL/FOL.thy	Sat Dec 31 21:49:39 2005 +0100
@@ -24,15 +24,6 @@
 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