src/HOL/Ord.ML
changeset 7990 0a604b2fc2b1
parent 7617 e783adccf39e
child 8024 199721f2eb2d