src/ZF/Ordinal.thy
changeset 2214 f869dc885841
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01