diff -r 646ea25ff59d -r 85ea2be46c71 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 *)