src/ZF/Ord.thy
changeset 7924 5fee69b1f5fe
parent 124 858ab9a9b047