theory Cardinal_Order_Relation_discontinued imports "HOL-Cardinals.Cardinal_Order_Relation" begin text ‹ This entry has been discontinued because it is now part of the Isabelle distribution. › end