1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Cardinals/Cardinals.thy	Tue Sep 18 13:38:10 2012 +0200
     1.3 @@ -0,0 +1,15 @@
     1.4 +(*  Title:      HOL/Cardinals/Cardinals.thy
     1.5 +    Author:     Andrei Popescu, TU Muenchen
     1.6 +    Author:     Dmitriy Traytel, TU Muenchen
     1.7 +    Copyright   2012
     1.8 +
     1.9 +Theory of ordinals and cardinals.
    1.10 +*)
    1.11 +
    1.12 +header {* Theory of Ordinals and Cardinals  *}
    1.13 +
    1.14 +theory Cardinals
    1.15 +imports Cardinal_Order_Relation Cardinal_Arithmetic
    1.16 +begin
    1.17 +
    1.18 +end

     2.1 --- a/src/HOL/ROOT	Tue Sep 18 11:42:22 2012 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Sep 18 13:38:10 2012 +0200
     2.3 @@ -604,7 +604,7 @@
     2.4  
     2.5  session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
     2.6    description {* Ordinals and Cardinals, Full Theories *}
     2.7 -  theories Cardinal_Order_Relation
     2.8 +  theories Cardinals
     2.9    files
    2.10      "document/intro.tex"
    2.11      "document/root.tex"