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.