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