src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 74245 282cd3aa6cc6
parent 69850 5f993636ac07
child 75624 22d1c5f2b9f4