src/Pure/term_ord.ML
changeset 34173 458ced35abb8
parent 32841 57dcddf81b01
child 35404 de56579ae229
equal deleted inserted replaced
34172:4301e9ea1c54 34173:458ced35abb8