src/ZF/Ord.thy
changeset 3333 0bbf06e86c06
parent 124 858ab9a9b047