| changeset 1478 | 2b8c2a7547ab |
| parent 484 | 70b789956bd3 |
| child 13134 | bf37a3049251 |
| 1477:4c51ab632cda | 1478:2b8c2a7547ab |
|---|---|
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 |
6 Cardinal Arithmetic WITH the Axiom of Choice |
7 *) |
7 *) |
8 |
8 |