src/HOL/Cardinals/Wellorder_Embedding_Base.thy
changeset 49890 89eff795f757
parent 49753 a344f1a21211
child 49922 b76937179ff5