src/HOL/Ord.ML
changeset 8042 ecdedff41e67
parent 8024 199721f2eb2d
child 8214 d612354445b6