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

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