--- a/src/HOL/Word/Misc_Typedef.thy Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Word/Misc_Typedef.thy Mon Sep 13 11:13:15 2010 +0200
@@ -53,14 +53,14 @@
lemma set_Rep:
"A = range Rep"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
show "(x \<in> A) = (x \<in> range Rep)"
by (auto dest: Abs_inverse [of x, symmetric])
qed
lemma set_Rep_Abs: "A = range (Rep o Abs)"
-proof (rule set_ext)
+proof (rule set_eqI)
fix x
show "(x \<in> A) = (x \<in> range (Rep o Abs))"
by (auto dest: Abs_inverse [of x, symmetric])