src/Pure/term_ord.ML
changeset 36895 a96f9793d9c5
parent 35408 b48ab741683b
child 37852 a902f158b4fc
equal deleted inserted replaced
36894:2f172cf4fb52 36895:a96f9793d9c5