src/HOL/Ord.ML
changeset 10379 93630e0c5ae9
parent 10231 178a272bceeb
child 10753 e43e017df8c1