src/ZF/Ordinal.thy
changeset 15166 66f0584aa714
parent 14864 419b45cdb400
child 16417 9bc16273c2d4