--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Cardinals/Cardinals.thy Tue Sep 18 13:38:10 2012 +0200
@@ -0,0 +1,15 @@
+(* Title: HOL/Cardinals/Cardinals.thy
+ Author: Andrei Popescu, TU Muenchen
+ Author: Dmitriy Traytel, TU Muenchen
+ Copyright 2012
+
+Theory of ordinals and cardinals.
+*)
+
+header {* Theory of Ordinals and Cardinals *}
+
+theory Cardinals
+imports Cardinal_Order_Relation Cardinal_Arithmetic
+begin
+
+end
--- a/src/HOL/ROOT Tue Sep 18 11:42:22 2012 +0200
+++ b/src/HOL/ROOT Tue Sep 18 13:38:10 2012 +0200
@@ -604,7 +604,7 @@
session "HOL-Cardinals" in Cardinals = "HOL-Cardinals-Base" +
description {* Ordinals and Cardinals, Full Theories *}
- theories Cardinal_Order_Relation
+ theories Cardinals
files
"document/intro.tex"
"document/root.tex"