# HG changeset patch
# User wenzelm
# Date 1136062179 -3600
# Node ID ce7b80b7c84eeac9a6a74e79dd0a8ea487fdc5a9
# Parent  d995aecddc15d7b3f92149527a5eda6e03acc2f4
removed obsolete cla_dist_concl;

diff -r d995aecddc15 -r ce7b80b7c84e 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
diff -r d995aecddc15 -r ce7b80b7c84e src/HOL/HOL.thy
--- 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