Major Section: ACL2 Documentation
Call this up with
defthmevent with an
instructionsparameter supplied; see the documentation for proof-checker command
"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:
The tutorial illustrates more than just the proof-checker. The portion relevant to the proof-checker may be accessed directly:
See set-evisc-tuple for how to arrange that output is printed in abbreviated
form. In general, the proof-checker uses the
described in that documentation.
Individual proof-checker commands are documented in subsection