src/ZF/Ord.ML
changeset 6829 50459a995aa3
parent 186 320f6bdb593a
equal deleted inserted replaced
6828:ea6832d74353 6829:50459a995aa3