## ACL2 System Architecture

The user interacts with the theorem prover by giving it definitions,
theorems and advice (e.g., ``use this lemma.''), often in the form
of books books .

The theorem prover uses the rules in the library of books the user has
selected.

The theorem prover prints its proof attempts to the user.

When a theorem is proved it is converted to a rule under the control
of the user's rule-classes .

**The informed user can make ACL2 do amazing things.**