src/ZF/Ordinal.thy
changeset 75400 970b9ab6c439
parent 71085 950e1cfe0fe4
child 76213 e44d86131648