src/HOL/Ord.ML
changeset 10621 3d15596ee644
parent 10231 178a272bceeb
child 10753 e43e017df8c1