src/ZF/Ord.thy
changeset 13509 6f168374652a
parent 124 858ab9a9b047