/src/HOL/Ordinals_and_Cardinals/
drwxr-xr-x [up]
drwxr-xr-x document
-rw-r--r-- 2012-08-30 15:44 +0900 31397 Cardinal_Arithmetic.thy
-rw-r--r-- 2012-08-30 15:44 +0900 38019 Cardinal_Order_Relation.thy
-rw-r--r-- 2012-08-30 15:44 +0900 91680 Cardinal_Order_Relation_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 27046 Constructions_on_Wellorders.thy
-rw-r--r-- 2012-08-30 15:44 +0900 60938 Constructions_on_Wellorders_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 5574 Fun_More.thy
-rw-r--r-- 2012-08-30 15:44 +0900 8475 Fun_More_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 18314 Order_Relation_More.thy
-rw-r--r-- 2012-08-30 15:44 +0900 9121 Order_Relation_More_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 10546 README.txt
-rw-r--r-- 2012-08-30 15:44 +0900 1735 TODO.txt
-rw-r--r-- 2012-08-30 15:44 +0900 1446 Wellfounded_More.thy
-rw-r--r-- 2012-08-30 15:44 +0900 7681 Wellfounded_More_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 5996 Wellorder_Embedding.thy
-rw-r--r-- 2012-08-30 15:44 +0900 42727 Wellorder_Embedding_Base.thy
-rw-r--r-- 2012-08-30 15:44 +0900 15553 Wellorder_Relation.thy
-rw-r--r-- 2012-08-30 15:44 +0900 18735 Wellorder_Relation_Base.thy