src/HOL/Ord.ML
changeset 10706 f02834001fca
parent 10231 178a272bceeb
child 10753 e43e017df8c1