src/ZF/ord.ML
changeset 6430 69400c97d3bf
parent 186 320f6bdb593a