Major Section: ACL2 Documentation

Call this up with `(verify ...)`

.

### DEFINE-PC-HELP -- define a macro command whose purpose is to print something

### DEFINE-PC-MACRO -- define a proof-checker macro command

### DEFINE-PC-META -- define a proof-checker meta command

### INSTRUCTIONS -- instructions to the proof checker

### MACRO-COMMAND -- compound command for the proof-checker

### PROOF-CHECKER-COMMANDS -- list of commands for the proof-checker

### RETRIEVE -- re-enter a (specified) proof-checker state

### TOGGLE-PC-MACRO -- change an ordinary macro command to an atomic macro, or vice-versa

### UNSAVE -- remove a proof-checker state

### VERIFY -- enter the interactive proof checker

`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.