src/HOL/Ord.ML
changeset 4571 6b02fc8a97f6
parent 4089 96fba19bcbe2
child 4600 e3e7e901ce6c