src/ZF/Ordinal.thy
changeset 783 08f1785a4384
parent 753 ec86863e87c8
child 852 664052e3cf66