src/ZF/AC/AC_Equiv.thy

--- a/src/ZF/AC/AC_Equiv.thy	Thu Jan 13 17:30:23 2000 +0100
+++ b/src/ZF/AC/AC_Equiv.thy	Thu Jan 13 17:31:30 2000 +0100
@@ -12,7 +12,10 @@
 but slightly changed.
 *)
 
-AC_Equiv = CardinalArith + Univ + 
+
+AC_Equiv = CardinalArith + Univ +
+           (*NOT "Main" because that theory includes AC!!!*)
+
 
 consts