src/Pure/term_ord.ML
changeset 31259 c1b981b71dba
parent 29269 5c25a2012975
child 31971 8c1b845ed105