| changeset 39302 | d7728f65b353 |
| parent 39223 | 022f16801e4e |
| child 39365 | 9cab71c20613 |
--- a/src/HOL/Nitpick.thy Mon Sep 13 08:43:48 2010 +0200 +++ b/src/HOL/Nitpick.thy Mon Sep 13 11:13:15 2010 +0200 @@ -58,7 +58,7 @@ lemma Ex1_def [nitpick_def, no_atp]: "Ex1 P \<equiv> \<exists>x. P = {x}" apply (rule eq_reflection) -apply (simp add: Ex1_def set_ext_iff) +apply (simp add: Ex1_def set_eq_iff) apply (rule iffI) apply (erule exE) apply (erule conjE)