src/HOL/Nitpick.thy
changeset 39198 f967a16dfcdd
parent 38393 7c045c03598f
child 39223 022f16801e4e
     1.1 --- a/src/HOL/Nitpick.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Sep 07 10:05:19 2010 +0200
     1.3 @@ -59,7 +59,7 @@
     1.4  lemma Ex1_def [nitpick_def, no_atp]:
     1.5  "Ex1 P \<equiv> \<exists>x. P = {x}"
     1.6  apply (rule eq_reflection)
     1.7 -apply (simp add: Ex1_def expand_set_eq)
     1.8 +apply (simp add: Ex1_def set_ext_iff)
     1.9  apply (rule iffI)
    1.10   apply (erule exE)
    1.11   apply (erule conjE)