src/ZF/ord.ML
changeset 11180 39d3b8e8ad5c
parent 186 320f6bdb593a
equal deleted inserted replaced
11179:bee6673b020a 11180:39d3b8e8ad5c