src/HOL/Nitpick.thy
changeset 39302 d7728f65b353
parent 39223 022f16801e4e
child 39365 9cab71c20613
     1.1 --- a/src/HOL/Nitpick.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Nitpick.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -58,7 +58,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 set_ext_iff)
     1.8 +apply (simp add: Ex1_def set_eq_iff)
     1.9  apply (rule iffI)
    1.10   apply (erule exE)
    1.11   apply (erule conjE)