src/ZF/Ord.ML
changeset 1868 836950047d85
parent 186 320f6bdb593a