--- a/src/HOL/HOL.thy Sat Aug 16 12:15:56 2014 +0200
+++ b/src/HOL/HOL.thy Sat Aug 16 13:23:50 2014 +0200
@@ -763,8 +763,6 @@
subsubsection {* Atomizing elimination rules *}
-setup AtomizeElim.setup
-
lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
by rule iprover+