src/ZF/Ord.thy
changeset 4648 f04da668581c
parent 124 858ab9a9b047