src/ZF/ord.thy
changeset 12160 a5cf3ea0685d
parent 124 858ab9a9b047