src/ZF/Ordinal.thy
changeset 1228 7d6b0241afab
parent 852 664052e3cf66
child 1401 0c439768f45c