src/ZF/Ordinal.thy
changeset 69690 1fb204399d8d
parent 69593 3dda49e08b9d
child 71085 950e1cfe0fe4