src/ZF/ord.thy
changeset 7760 43f8d28dbc6e
parent 124 858ab9a9b047