src/HOL/Ord.ML
changeset 7596 c97c3ad15d2e
parent 7494 45905028bb1d
child 7617 e783adccf39e
equal deleted inserted replaced
7595:5f5d575ddac3 7596:c97c3ad15d2e