--- a/src/FOL/IFOL.thy Sat Aug 16 12:15:56 2014 +0200
+++ b/src/FOL/IFOL.thy Sat Aug 16 13:23:50 2014 +0200
@@ -710,16 +710,14 @@
subsection {* Atomizing elimination rules *}
-setup AtomizeElim.setup
-
lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
-by rule iprover+
+ by rule iprover+
lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
-by rule iprover+
+ by rule iprover+
lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
-by rule iprover+
+ by rule iprover+
lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..