src/ZF/Ordinal.thy
changeset 75513 36316c6a3fc2
parent 71085 950e1cfe0fe4
child 76213 e44d86131648