# HG changeset patch
# User popescua
# Date 1347968290 -7200
# Node ID 80b1963215c8f139868e762ed9fb42168f12c02f
# Parent  5bc80d96241ea390045b8d4ee15d9cf92218e754
added top-level theory for Cardinals

diff -r 5bc80d96241e -r 80b1963215c8 src/HOL/Cardinals/Cardinals.thy
--- /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
diff -r 5bc80d96241e -r 80b1963215c8 src/HOL/ROOT
--- 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"