src/HOL/Cardinals/Wellorder_Embedding.thy
changeset 58984 ae0c56c485ae
parent 58889 5b7a9633cfa8
child 60585 48fdff264eb2