AC Unification in hol90

We report on an implementation of associative-commutative unification in an LCF-style theorem prover. We show how this algorithm can be used to implement rewriting modulo associativity and commutativity. This is an example of the sound incorporation of automatic first order methods into an interactive higher-order logic theorem prover.