src/HOL/Ord.ML
changeset 7584 5be4bb8e4e3f
parent 7494 45905028bb1d
child 7617 e783adccf39e