src/ZF/Ordinal.thy
changeset 61578 6623c81cb15a
parent 61402 520a28294168
child 61798 27f3c10b0b50