src/ZF/Cardinal_AC.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
--- a/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:03:21 2002 +0200
+++ b/src/ZF/Cardinal_AC.thy	Tue Jul 09 23:05:26 2002 +0200
@@ -3,11 +3,11 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
-Cardinal Arithmetic WITH the Axiom of Choice
-
 These results help justify infinite-branching datatypes
 *)
 
+header{*Cardinal Arithmetic Using AC*}
+
 theory Cardinal_AC = CardinalArith + Zorn:
 
 (*** Strengthened versions of existing theorems about cardinals ***)