| author | popescua |
| Tue, 18 Sep 2012 13:38:10 +0200 | |
| changeset 50454 | 80b1963215c8 |
| child 55918 | 483131676087 |
| permissions | -rw-r--r-- |
| popescua@50454 | 1 |
(* Title: HOL/Cardinals/Cardinals.thy |
| popescua@50454 | 2 |
Author: Andrei Popescu, TU Muenchen |
| popescua@50454 | 3 |
Author: Dmitriy Traytel, TU Muenchen |
| popescua@50454 | 4 |
Copyright 2012 |
| popescua@50454 | 5 |
|
| popescua@50454 | 6 |
Theory of ordinals and cardinals. |
| popescua@50454 | 7 |
*) |
| popescua@50454 | 8 |
|
| popescua@50454 | 9 |
header {* Theory of Ordinals and Cardinals *}
|
| popescua@50454 | 10 |
|
| popescua@50454 | 11 |
theory Cardinals |
| popescua@50454 | 12 |
imports Cardinal_Order_Relation Cardinal_Arithmetic |
| popescua@50454 | 13 |
begin |
| popescua@50454 | 14 |
|
| popescua@50454 | 15 |
end |