equal
deleted
inserted
replaced
1 (* Title: ZF/Cardinal_AC.thy |
1 (* Title: ZF/Cardinal_AC.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Cardinal Arithmetic WITH the Axiom of Choice |
|
7 |
|
8 These results help justify infinite-branching datatypes |
6 These results help justify infinite-branching datatypes |
9 *) |
7 *) |
|
8 |
|
9 header{*Cardinal Arithmetic Using AC*} |
10 |
10 |
11 theory Cardinal_AC = CardinalArith + Zorn: |
11 theory Cardinal_AC = CardinalArith + Zorn: |
12 |
12 |
13 (*** Strengthened versions of existing theorems about cardinals ***) |
13 (*** Strengthened versions of existing theorems about cardinals ***) |
14 |
14 |