src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 81030 88879ff1cef5
parent 80932 261cd8722677
child 81125 ec121999a9cb