src/ZF/Ord.thy
changeset 2230 275a5a699ff7
parent 124 858ab9a9b047
equal deleted inserted replaced
2229:64acb485ecce 2230:275a5a699ff7