--- a/src/ZF/AC.thy Thu Mar 15 15:54:22 2012 +0000
+++ b/src/ZF/AC.thy Thu Mar 15 16:35:02 2012 +0000
@@ -9,7 +9,7 @@
text{*This definition comes from Halmos (1960), page 59.*}
axiomatization where
- AC: "[| a: A; !!x. x:A ==> (\<exists>y. y:B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
+ AC: "[| a \<in> A; !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"
(*The same as AC, but no premise @{term"a \<in> A"}*)
lemma AC_Pi: "[| !!x. x \<in> A ==> (\<exists>y. y \<in> B(x)) |] ==> \<exists>z. z \<in> Pi(A,B)"