# Expander

Routines for simplifying terms.

NOTE: If you are looking for a simple interface to the ACL2
rewriter, see rewrite$.

The routines provided by the expander can be useful in generating
theorems and simplifying expressions, under given assumptions.

They were developed rather in a hurry and should be used without expecting
the usual standards of care present in development of ACL2 code. Once these
routines are used to generate theorems for you, you should check the theorems
directly with ACL2.

To load the expander, run:

(include-book "misc/expander" :dir :system)

### Subtopics

- Defthm?
- Generate a theorem.
- Symsim
- Simplify given term and hypotheses.