| changeset 2469 | b50b8c0eec01 |
| parent 1478 | 2b8c2a7547ab |
| child 3892 | 1d184682ac9f |
--- a/src/ZF/AC/DC.thy Fri Jan 03 10:48:28 1997 +0100 +++ b/src/ZF/AC/DC.thy Fri Jan 03 15:01:55 1997 +0100 @@ -5,7 +5,7 @@ Theory file for the proofs concernind the Axiom of Dependent Choice *) -DC = AC_Equiv + Hartog + first + Cardinal_aux + "DC_lemmas" + +DC = AC_Equiv + Hartog + Cardinal_aux + "DC_lemmas" + consts