src/ZF/Ord.thy
changeset 13535 007559e981c7
parent 124 858ab9a9b047