src/ZF/Ordinal.ML
changeset 9805 10b617bdd028
parent 9492 72e429c66608
child 9842 58d8335cc40c