PROOF-CHECKER

support for low-level interaction 
Major Section:  ACL2 Documentation

Call this up with (verify ...).

Some Related Topics

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; see the documentation for proof-checker command exit (in package "ACL2-PC"). Such an event can be replayed later in a new ACL2 session with the ``proof-checker'' loaded.

A tutorial is available on the world-wide web:
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html.
The tutorial illustrates more than just the proof-checker. The portion relevant to the proof-checker may be accessed directly:
http://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#slide29

See set-evisc-tuple for how to arrange that output is printed in abbreviated form. In general, the proof-checker uses the :TERM evisc-tuple described in that documentation.

Individual proof-checker commands are documented in subsection proof-checker-commands.