src/ZF/ord.thy
changeset 777 c007eba368b7
parent 124 858ab9a9b047