Session Wetzels_Problem

Theories

• 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.ZFC_Typeclasses
• ZFC_in_HOL.General_Cardinals
• Wetzels_Problem