src/HOL/Ord.ML
changeset 3718 d78cf498a88c
parent 2935 998cb95fdd43
child 4089 96fba19bcbe2
equal deleted inserted replaced
3717:e28553315355 3718:d78cf498a88c