src/Pure/term_ord.ML
changeset 29738 05d5615e12d3
parent 29269 5c25a2012975
child 31971 8c1b845ed105