src/ZF/Ordinal.thy
changeset 13046 69ab0e74ccda
parent 12114 a8e860c86252
child 13155 dcbf6cb95534