src/HOL/Cardinals/Cardinals.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63167 0909deb8059b
permissions -rw-r--r--
more permissive;
popescua@49439
     1
(*  Title:      HOL/Cardinals/Cardinals.thy
popescua@49439
     2
    Author:     Andrei Popescu, TU Muenchen
popescua@49439
     3
    Author:     Dmitriy Traytel, TU Muenchen
popescua@49439
     4
    Copyright   2012
popescua@49439
     5
popescua@49439
     6
Theory of ordinals and cardinals.
popescua@49439
     7
*)
popescua@49439
     8
wenzelm@63167
     9
section \<open>Theory of Ordinals and Cardinals\<close>
popescua@49439
    10
popescua@49439
    11
theory Cardinals
traytel@54980
    12
imports Ordinal_Arithmetic Cardinal_Arithmetic Wellorder_Extension
popescua@49439
    13
begin
popescua@49439
    14
popescua@49439
    15
end