src/ZF/Ordinal.thy
changeset 74516 2c093a3167d1
parent 71085 950e1cfe0fe4
child 76213 e44d86131648