equal
deleted
inserted
replaced
1 (* Title: ZF/Cardinal.thy |
1 (* Title: ZF/Cardinal.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 Cardinals in Zermelo-Fraenkel Set Theory |
|
7 |
|
8 This theory does NOT assume the Axiom of Choice |
|
9 *) |
6 *) |
|
7 |
|
8 header{*Cardinal Numbers Without the Axiom of Choice*} |
10 |
9 |
11 theory Cardinal = OrderType + Finite + Nat + Sum: |
10 theory Cardinal = OrderType + Finite + Nat + Sum: |
12 |
11 |
13 (*** The following really belong in upair ***) |
12 (*** The following really belong in upair ***) |
14 |
13 |