Term Rewriting and All That
ML programs, by chapter
: a library of basic ML functions.
: lexicographic and multiset orders.
: terms, unification, matching, normalization.
: term orders.
: Critical Pairs.
: Knuth-Bendix completion à la Huet.
: combination of decision procedures for word problems.
: Boolean unification.
ML for the Working Programmer
General information on ML