src/ZF/Cardinal_AC.thy
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