src/Pure/term_ord.ML
changeset 34173 458ced35abb8
parent 32841 57dcddf81b01
child 35404 de56579ae229