Session Ordinal_Partitions
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Product_Lexorder
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.Infinite_Set
HOL-Library.Countable_Set
HOL-Library.FuncSet
HOL-Library.Equipollence
HOL-Cardinals.Fun_More
HOL-Cardinals.Order_Relation_More
HOL-Cardinals.Wellfounded_More
HOL-Cardinals.Wellorder_Relation
HOL-Cardinals.Wellorder_Embedding
HOL-Cardinals.Order_Union
HOL-Cardinals.Wellorder_Constructions
HOL-Cardinals.Ordinal_Arithmetic
HOL-Cardinals.Cardinal_Order_Relation
HOL-Cardinals.Cardinal_Arithmetic
HOL-Cardinals.Wellorder_Extension
HOL-Cardinals.Cardinals
ZFC_in_HOL.ZFC_Library
ZFC_in_HOL.ZFC_in_HOL
ZFC_in_HOL.ZFC_Cardinals
ZFC_in_HOL.Kirby
ZFC_in_HOL.Ordinal_Exp
HOL-Library.Ramsey
Nash_Williams.Nash_Extras
Nash_Williams.Nash_Williams
Library_Additions
ZFC_in_HOL.ZFC_Typeclasses
ZFC_in_HOL.Cantor_NF
Partitions
Erdos_Milner
Omega_Omega