--- a/src/ZF/AC/DC_lemmas.thy Thu Oct 16 13:42:53 1997 +0200 +++ b/src/ZF/AC/DC_lemmas.thy Thu Oct 16 13:43:42 1997 +0200 @@ -1,4 +1,3 @@ (*Dummy theory to document dependencies *) -DC_lemmas = AC_Equiv - +DC_lemmas = AC_Equiv + Cardinal_aux