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. Such an event can be replayed later in a new
ACL2 session with the ``proof-checker'' loaded.
Individual proof-checker commands are documented in subsection
proof-checker-commands.