src/HOL/Cardinals/Constructions_on_Wellorders.thy
changeset 57000 c914618feef8
parent 55102 761e40ce91bc