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