--- a/src/ZF/AC/AC_Equiv.thy Mon Dec 07 10:19:30 2015 +0100
+++ b/src/ZF/AC/AC_Equiv.thy Mon Dec 07 10:23:50 2015 +0100
@@ -124,7 +124,7 @@
assumes AC18: "A\<noteq>0 & (\<forall>a \<in> A. B(a) \<noteq> 0) \<longrightarrow>
((\<Inter>a \<in> A. \<Union>b \<in> B(a). X(a,b)) =
(\<Union>f \<in> \<Pi> a \<in> A. B(a). \<Inter>a \<in> A. X(a, f`a)))"
- --"AC18 cannot be expressed within the object-logic"
+ \<comment>"AC18 cannot be expressed within the object-logic"
definition
"AC19 == \<forall>A. A\<noteq>0 & 0\<notin>A \<longrightarrow> ((\<Inter>a \<in> A. \<Union>b \<in> a. b) =