src/ZF/ord.thy
changeset 8849 f1933a670ae4
parent 124 858ab9a9b047