# HG changeset patch
# User wenzelm
# Date 1135958216 -3600
# Node ID 9bdfb6eaf8ab6530bd06b9c584beb2083f0153da
# Parent  ee14a65fe764648ccb65fce18443918d26c0ec52
provide cla_dist_concl;

diff -r ee14a65fe764 -r 9bdfb6eaf8ab src/FOL/FOL.thy
--- 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
diff -r ee14a65fe764 -r 9bdfb6eaf8ab src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Fri Dec 30 16:56:54 2005 +0100
+++ b/src/FOL/cladata.ML	Fri Dec 30 16:56:56 2005 +0100
@@ -9,7 +9,7 @@
 section "Classical Reasoner";
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun(val classical = classical);
+structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
   compatibility with strange things done in many existing proofs *)
diff -r ee14a65fe764 -r 9bdfb6eaf8ab src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Fri Dec 30 16:56:54 2005 +0100
+++ b/src/HOL/HOL.thy	Fri Dec 30 16:56:56 2005 +0100
@@ -909,6 +909,15 @@
 
 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
 
diff -r ee14a65fe764 -r 9bdfb6eaf8ab src/HOL/cladata.ML
--- a/src/HOL/cladata.ML	Fri Dec 30 16:56:54 2005 +0100
+++ b/src/HOL/cladata.ML	Fri Dec 30 16:56:56 2005 +0100
@@ -38,7 +38,7 @@
 
 
 (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
-structure Make_Elim = Make_Elim_Fun (val classical = classical);
+structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
 
 (*we don't redeclare the original make_elim (Tactic.make_elim) for 
   compatibliity with strange things done in many existing proofs *)