src/ZF/AC/AC7_AC9.thy

--- a/src/ZF/AC/AC7_AC9.thy	Mon Jul 21 16:30:49 2008 +0200
+++ b/src/ZF/AC/AC7_AC9.thy	Fri Jul 25 07:35:53 2008 +0200
@@ -6,7 +6,9 @@
 instances of AC.
 *)
 
-theory AC7_AC9 imports AC_Equiv begin
+theory AC7_AC9
+imports AC_Equiv
+begin
 
 (* ********************************************************************** *)
 (* Lemmas used in the proofs AC7 ==> AC6 and AC9 ==> AC1                  *)