src/ZF/Ord.thy
changeset 13076 70704dd48bd5
parent 124 858ab9a9b047