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.
