src/Pure/term_ord.ML
changeset 31013 69a476d6fea6
parent 29269 5c25a2012975
child 31971 8c1b845ed105