src/HOL/Cardinals/Wellorder_Embedding.thy
changeset 76371 1ac2416e8432
parent 68652 1e37b45ce3fb
child 76948 f33df7529fed