src/ZF/CardinalArith.thy
changeset 13328 703de709a64b
parent 13269 3ba9be497c33
child 13356 c9cfe1638bf2
     1.1 --- a/src/ZF/CardinalArith.thy	Tue Jul 09 23:03:21 2002 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Tue Jul 09 23:05:26 2002 +0200
     1.3 @@ -3,13 +3,9 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1994  University of Cambridge
     1.6  
     1.7 -Cardinal arithmetic -- WITHOUT the Axiom of Choice
     1.8 +*)
     1.9  
    1.10 -Note: Could omit proving the algebraic laws for cardinal addition and
    1.11 -multiplication.  On finite cardinals these operations coincide with
    1.12 -addition and multiplication of natural numbers; on infinite cardinals they
    1.13 -coincide with union (maximum).  Either way we get most laws for free.
    1.14 -*)
    1.15 +header{*Cardinal Arithmetic Without the Axiom of Choice*}
    1.16  
    1.17  theory CardinalArith = Cardinal + OrderArith + ArithSimp + Finite:
    1.18  
    1.19 @@ -94,6 +90,11 @@
    1.20  
    1.21  (*** Cardinal addition ***)
    1.22  
    1.23 +text{*Note: Could omit proving the algebraic laws for cardinal addition and
    1.24 +multiplication.  On finite cardinals these operations coincide with
    1.25 +addition and multiplication of natural numbers; on infinite cardinals they
    1.26 +coincide with union (maximum).  Either way we get most laws for free.*}
    1.27 +
    1.28  (** Cardinal addition is commutative **)
    1.29  
    1.30  lemma sum_commute_eqpoll: "A+B \<approx> B+A"