--- a/src/HOL/ZF/HOLZF.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/ZF/HOLZF.thy Mon Sep 13 11:13:15 2010 +0200
@@ -155,7 +155,7 @@
by (auto simp add: explode_def)
lemma explode_CartProd_eq: "explode (CartProd a b) = (% (x,y). Opair x y) ` ((explode a) \<times> (explode b))"
- by (simp add: explode_def set_ext_iff CartProd image_def)
+ by (simp add: explode_def set_eq_iff CartProd image_def)
lemma explode_Repl_eq: "explode (Repl A f) = image f (explode A)"
by (simp add: explode_def Repl image_def)
@@ -830,7 +830,7 @@
apply (subst set_like_def)
apply (auto simp add: image_def)
apply (rule_tac x="Sep (Ext_ZF_hull R y) (\<lambda> z. z \<in> (Ext (R^+) y))" in exI)
- apply (auto simp add: explode_def Sep set_ext
+ apply (auto simp add: explode_def Sep set_eqI
in_Ext_RTrans_implies_Elem_Ext_ZF_hull)
done