src/HOL/Cardinals/Constructions_on_Wellorders.thy
changeset 56747 f87e3be0de9a
parent 55102 761e40ce91bc