src/ZF/Ordinal.thy
changeset 75629 11e233ba53c8
parent 71085 950e1cfe0fe4
child 76213 e44d86131648