src/ZF/Ord.thy
changeset 9982 1860276fc8de
parent 124 858ab9a9b047