support for low-level interaction
Major Section:  ACL2 Documentation

Call this up with (verify ...).

This is an interactive system for checking theorems in ACL2. One enters it using VERIFY; see verify. The result of an interactive session is a defthm event with an :instructions parameter supplied. Such an event can be replayed later in a new ACL2 session with the ``proof-checker'' loaded.

Individual proof-checker commands have already been listed above. Among them are proof-checker commands help, help-long, more, and more!, which behave respectively like the ACL2 functions :doc, :doc!, :more, and :more!.