src/ZF/ord.ML
changeset 5395 b890c27c93d6
parent 186 320f6bdb593a