src/ZF/Ordinal.thy
changeset 12883 3f86b73d592d
parent 12114 a8e860c86252
child 13155 dcbf6cb95534