src/ZF/ord.thy
changeset 2246 fce7e34db8c8
parent 124 858ab9a9b047