changeset 484 | 70b789956bd3 |
child 1478 | 2b8c2a7547ab |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Cardinal_AC.thy Tue Jul 26 13:21:20 1994 +0200 @@ -0,0 +1,9 @@ +(* Title: ZF/Cardinal_AC.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Cardinal Arithmetic WITH the Axiom of Choice +*) + +Cardinal_AC = CardinalArith + Zorn