src/Pure/term_ord.ML
changeset 35160 6eb2b6c1d2d5
parent 32841 57dcddf81b01
child 35404 de56579ae229
equal deleted inserted replaced
35159:df38e92af926 35160:6eb2b6c1d2d5