1.1 --- a/src/HOL/HOL.thy	Tue Apr 08 15:47:15 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue Apr 08 18:30:40 2008 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    "~~/src/Provers/quantifier1.ML"
     1.5    ("simpdata.ML")
     1.6    "~~/src/Tools/random_word.ML"
     1.7 +  "~~/src/Tools/atomize_elim.ML"
     1.8    "~~/src/Tools/induct.ML"
     1.9    "~~/src/Tools/code/code_name.ML"
    1.10    "~~/src/Tools/code/code_funcgr.ML"
    1.11 @@ -879,6 +880,22 @@
    1.12    and [symmetric, defn] = atomize_all atomize_imp atomize_eq
    1.13  
    1.14  
    1.15 +subsubsection {* Atomizing elimination rules *}
    1.16 +
    1.17 +setup AtomizeElim.setup
    1.18 +
    1.19 +lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
    1.20 +  by rule iprover+
    1.21 +
    1.22 +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
    1.23 +  by rule iprover+
    1.24 +
    1.25 +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
    1.26 +  by rule iprover+
    1.27 +
    1.28 +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" ..
    1.29 +
    1.30 +
    1.31  subsection {* Package setup *}
    1.32  
    1.33  subsubsection {* Classical Reasoner setup *}