src/Pure/term_ord.ML
changeset 42266 f87e0be80a3f
parent 37852 a902f158b4fc
child 43794 49cbbe2768a8
equal deleted inserted replaced
42265:ffdaa07cf6cf 42266:f87e0be80a3f