src/HOL/Cardinals/Cardinal_Order_Relation.thy
changeset 78731 508c6ee2b6fb
parent 76951 293caf3dbecd