src/HOL/Ord.ML
changeset 3339 cfa72a70f2b5
parent 2935 998cb95fdd43
child 4089 96fba19bcbe2