src/ZF/ord.ML
changeset 3131 1ffa0963e6a4
parent 186 320f6bdb593a
equal deleted inserted replaced
3130:1ffe03f4c700 3131:1ffa0963e6a4