src/ZF/Ordinal.thy
changeset 23211 4d56ad10b5e8
parent 22808 a7daa74e2980
child 24893 b8ef7afe3a6b
equal deleted inserted replaced
23210:a0cb15114e7a 23211:4d56ad10b5e8