--- a/src/HOL/Complete_Lattice.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Complete_Lattice.thy Mon Sep 13 11:13:15 2010 +0200
@@ -272,7 +272,7 @@
lemma Union_eq:
"\<Union>A = {x. \<exists>B \<in> A. x \<in> B}"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
@@ -508,7 +508,7 @@
lemma Inter_eq:
"\<Inter>A = {x. \<forall>B \<in> A. x \<in> B}"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto