src/HOL/Ord.ML
changeset 10212 33fe2d701ddd
parent 9969 4753185f1dd2
child 10231 178a272bceeb
equal deleted inserted replaced
10211:1bece7f35762 10212:33fe2d701ddd