src/ZF/ord.ML
changeset 238 6af40e3a2bcb
parent 186 320f6bdb593a