src/HOL/Cardinals/Constructions_on_Wellorders.thy
changeset 57537 810bc6c41ebd
parent 55102 761e40ce91bc