src/ZF/Ord.thy
changeset 3992 8b87ba92f7a1
parent 124 858ab9a9b047