src/HOL/Cardinals/Constructions_on_Wellorders.thy
changeset 57978 8f4a332500e4
parent 55102 761e40ce91bc