src/Pure/term_ord.ML
changeset 33126 bb8806eb5da7
parent 32841 57dcddf81b01
child 35404 de56579ae229