--- a/src/ZF/AC/AC_Equiv.thy Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/AC_Equiv.thy Fri Jun 17 16:12:49 2005 +0200
@@ -12,7 +12,7 @@
but slightly changed.
*)
-theory AC_Equiv = Main: (*obviously not Main_ZFC*)
+theory AC_Equiv imports Main begin (*obviously not Main_ZFC*)
constdefs