menu

Fun_More
Order_Relation_More
Wellfounded_More
Wellorder_Relation
Wellorder_Embedding
Order_Union
Wellorder_Constructions
Ordinal_Arithmetic
Cardinal_Order_Relation
Cardinal_Arithmetic
Wellorder_Extension
Cardinals
Bounded_Set

HOL-Cardinals.Ordinal_Arithmetic

HTML Presentation