src/ZF/AC/DC.thy

--- a/src/ZF/AC/DC.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/AC/DC.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -5,7 +5,7 @@
 The proofs concerning the Axiom of Dependent Choice
 *)
 
-theory DC = AC_Equiv + Hartog + Cardinal_aux:
+theory DC imports AC_Equiv Hartog Cardinal_aux begin
 
 lemma RepFun_lepoll: "Ord(a) ==> {P(b). b \<in> a} \<lesssim> a"
 apply (unfold lepoll_def)