# HG changeset patch
# User wenzelm
# Date 1206567601 -3600
# Node ID cd74690f3bfbe6139c81f10b14b8e1300a0c89f1
# Parent  40932ee97ff83716330c0ce2311cbe738ba32381
pass imp_elim, swap to classical prover;

diff -r 40932ee97ff8 -r cd74690f3bfb src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Wed Mar 26 22:39:58 2008 +0100
+++ b/src/FOL/FOL.thy	Wed Mar 26 22:40:01 2008 +0100
@@ -163,6 +163,12 @@
   qed
 qed
 
+lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+  by (rule classical) iprover
+
+lemma swap: "~ P ==> (~ R ==> P) ==> R"
+  by (rule classical) iprover
+
 use "cladata.ML"
 setup Cla.setup
 setup cla_setup
diff -r 40932ee97ff8 -r cd74690f3bfb src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Wed Mar 26 22:39:58 2008 +0100
+++ b/src/FOL/cladata.ML	Wed Mar 26 22:40:01 2008 +0100
@@ -10,13 +10,14 @@
 
 (*** Applying ClassicalFun to create a classical prover ***)
 structure Classical_Data = 
-  struct
-  val mp        = @{thm mp}
+struct
+  val imp_elim  = @{thm imp_elim}
   val not_elim  = @{thm notE}
+  val swap      = @{thm swap}
   val classical = @{thm classical}
   val sizef     = size_of_thm
   val hyp_subst_tacs=[hyp_subst_tac]
-  end;
+end;
 
 structure Cla = ClassicalFun(Classical_Data);
 structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
diff -r 40932ee97ff8 -r cd74690f3bfb src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Mar 26 22:39:58 2008 +0100
+++ b/src/HOL/HOL.thy	Wed Mar 26 22:40:01 2008 +0100
@@ -883,6 +883,12 @@
 
 subsubsection {* Classical Reasoner setup *}
 
+lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
+  by (rule classical) iprover
+
+lemma swap: "~ P ==> (~ R ==> P) ==> R"
+  by (rule classical) iprover
+
 lemma thin_refl:
   "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
@@ -893,21 +899,22 @@
   val dest_eq = HOLogic.dest_eq
   val dest_Trueprop = HOLogic.dest_Trueprop
   val dest_imp = HOLogic.dest_imp
-  val eq_reflection = @{thm HOL.eq_reflection}
-  val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq}
-  val imp_intr = @{thm HOL.impI}
-  val rev_mp = @{thm HOL.rev_mp}
-  val subst = @{thm HOL.subst}
-  val sym = @{thm HOL.sym}
+  val eq_reflection = @{thm eq_reflection}
+  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
+  val imp_intr = @{thm impI}
+  val rev_mp = @{thm rev_mp}
+  val subst = @{thm subst}
+  val sym = @{thm sym}
   val thin_refl = @{thm thin_refl};
 end);
 open Hypsubst;
 
 structure Classical = ClassicalFun(
 struct
-  val mp = @{thm HOL.mp}
-  val not_elim = @{thm HOL.notE}
-  val classical = @{thm HOL.classical}
+  val imp_elim = @{thm imp_elim}
+  val not_elim = @{thm notE}
+  val swap = @{thm swap}
+  val classical = @{thm classical}
   val sizef = Drule.size_of_thm
   val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
 end);
@@ -996,8 +1003,8 @@
   type claset = Classical.claset
   val equality_name = @{const_name "op ="}
   val not_name = @{const_name Not}
-  val notE = @{thm HOL.notE}
-  val ccontr = @{thm HOL.ccontr}
+  val notE = @{thm notE}
+  val ccontr = @{thm ccontr}
   val contr_tac = Classical.contr_tac
   val dup_intr = Classical.dup_intr
   val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac