src/HOL/Ord.ML
changeset 8657 b9475dad85ed
parent 8529 4656e8312ba9
child 9242 c472ed4edded