changeset 3892 | 1d184682ac9f |
parent 2469 | b50b8c0eec01 |
child 5482 | 73dc3b2a7102 |
--- a/src/ZF/AC/DC.thy Thu Oct 16 13:42:53 1997 +0200 +++ b/src/ZF/AC/DC.thy Thu Oct 16 13:43:42 1997 +0200 @@ -5,7 +5,7 @@ Theory file for the proofs concernind the Axiom of Dependent Choice *) -DC = AC_Equiv + Hartog + Cardinal_aux + "DC_lemmas" + +DC = AC_Equiv + Hartog + Cardinal_aux + DC_lemmas + consts