1.1 --- a/src/HOL/HOL.thy	Wed Mar 26 22:39:58 2008 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Mar 26 22:40:01 2008 +0100
     1.3 @@ -883,6 +883,12 @@
     1.4  
     1.5  subsubsection {* Classical Reasoner setup *}
     1.6  
     1.7 +lemma imp_elim: "P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R"
     1.8 +  by (rule classical) iprover
     1.9 +
    1.10 +lemma swap: "~ P ==> (~ R ==> P) ==> R"
    1.11 +  by (rule classical) iprover
    1.12 +
    1.13  lemma thin_refl:
    1.14    "\<And>X. \<lbrakk> x=x; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
    1.15  
    1.16 @@ -893,21 +899,22 @@
    1.17    val dest_eq = HOLogic.dest_eq
    1.18    val dest_Trueprop = HOLogic.dest_Trueprop
    1.19    val dest_imp = HOLogic.dest_imp
    1.20 -  val eq_reflection = @{thm HOL.eq_reflection}
    1.21 -  val rev_eq_reflection = @{thm HOL.meta_eq_to_obj_eq}
    1.22 -  val imp_intr = @{thm HOL.impI}
    1.23 -  val rev_mp = @{thm HOL.rev_mp}
    1.24 -  val subst = @{thm HOL.subst}
    1.25 -  val sym = @{thm HOL.sym}
    1.26 +  val eq_reflection = @{thm eq_reflection}
    1.27 +  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
    1.28 +  val imp_intr = @{thm impI}
    1.29 +  val rev_mp = @{thm rev_mp}
    1.30 +  val subst = @{thm subst}
    1.31 +  val sym = @{thm sym}
    1.32    val thin_refl = @{thm thin_refl};
    1.33  end);
    1.34  open Hypsubst;
    1.35  
    1.36  structure Classical = ClassicalFun(
    1.37  struct
    1.38 -  val mp = @{thm HOL.mp}
    1.39 -  val not_elim = @{thm HOL.notE}
    1.40 -  val classical = @{thm HOL.classical}
    1.41 +  val imp_elim = @{thm imp_elim}
    1.42 +  val not_elim = @{thm notE}
    1.43 +  val swap = @{thm swap}
    1.44 +  val classical = @{thm classical}
    1.45    val sizef = Drule.size_of_thm
    1.46    val hyp_subst_tacs = [Hypsubst.hyp_subst_tac]
    1.47  end);
    1.48 @@ -996,8 +1003,8 @@
    1.49    type claset = Classical.claset
    1.50    val equality_name = @{const_name "op ="}
    1.51    val not_name = @{const_name Not}
    1.52 -  val notE = @{thm HOL.notE}
    1.53 -  val ccontr = @{thm HOL.ccontr}
    1.54 +  val notE = @{thm notE}
    1.55 +  val ccontr = @{thm ccontr}
    1.56    val contr_tac = Classical.contr_tac
    1.57    val dup_intr = Classical.dup_intr
    1.58    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac