--- a/src/ZF/AC/AC17_AC1.thy Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC17_AC1.thy Fri Jul 25 07:35:53 2008 +0200
@@ -8,7 +8,9 @@
to AC0 and AC1.
*)
-theory AC17_AC1 imports HH begin
+theory AC17_AC1
+imports HH
+begin
(** AC0 is equivalent to AC1.