src/ZF/ord.ML
changeset 12873 d7f8dfaad46d
parent 186 320f6bdb593a