src/ZF/Ordinal.thy
changeset 16090 fbb5ae140535
parent 14864 419b45cdb400
child 16417 9bc16273c2d4