src/ZF/ord.thy
changeset 13480 bb72bd43c6c3
parent 124 858ab9a9b047