src/HOL/Ord.ML
changeset 8657 b9475dad85ed
parent 8529 4656e8312ba9
child 9242 c472ed4edded
equal deleted inserted replaced
8656:1062572b5b37 8657:b9475dad85ed