src/ZF/Ordinal.thy
changeset 71222 2bc39c80a95d
parent 71085 950e1cfe0fe4
child 76213 e44d86131648