src/HOL/HOL.thy
changeset 57948 75724d71013c
parent 57512 cc97b347b301
child 57962 0284a7d083be
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 16 12:15:56 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 13:23:50 2014 +0200
     1.3 @@ -763,8 +763,6 @@
     1.4  
     1.5  subsubsection {* Atomizing elimination rules *}
     1.6  
     1.7 -setup AtomizeElim.setup
     1.8 -
     1.9  lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
    1.10    by rule iprover+
    1.11