Major Section: ACL2 Documentation

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

.

### ACL2-PC::= -- (atomic macro)

### ACL2-PC::ACL2-WRAP -- (macro)

`(lisp x)`

### ACL2-PC::ADD-ABBREVIATION -- (primitive)

### ACL2-PC::BASH -- (atomic macro)

### ACL2-PC::BDD -- (atomic macro)

### ACL2-PC::BK -- (atomic macro)

### ACL2-PC::BOOKMARK -- (macro)

### ACL2-PC::CASESPLIT -- (primitive)

### ACL2-PC::CG -- (macro)

### ACL2-PC::CHANGE-GOAL -- (primitive)

### ACL2-PC::CLAIM -- (atomic macro)

### ACL2-PC::COMM -- (macro)

### ACL2-PC::COMMANDS -- (macro)

### ACL2-PC::COMMENT -- (primitive)

### ACL2-PC::CONTRADICT -- (macro)

`contrapose`

### ACL2-PC::CONTRAPOSE -- (primitive)

### ACL2-PC::DEMOTE -- (primitive)

### ACL2-PC::DIVE -- (primitive)

### ACL2-PC::DO-ALL -- (macro)

### ACL2-PC::DO-ALL-NO-PROMPT -- (macro)

### ACL2-PC::DO-STRICT -- (macro)

### ACL2-PC::DROP -- (primitive)

### ACL2-PC::DV -- (atomic macro)

### ACL2-PC::ELIM -- (atomic macro)

### ACL2-PC::EQUIV -- (primitive)

### ACL2-PC::EX -- (macro)

### ACL2-PC::EXIT -- (meta)

### ACL2-PC::EXPAND -- (primitive)

### ACL2-PC::FAIL -- (macro)

### ACL2-PC::FORWARDCHAIN -- (atomic macro)

### ACL2-PC::FREE -- (atomic macro)

### ACL2-PC::GENERALIZE -- (primitive)

### ACL2-PC::GOALS -- (macro)

### ACL2-PC::HELP -- (macro)

### ACL2-PC::HELP! -- (macro)

### ACL2-PC::HELP-LONG -- (macro)

`help!`

### ACL2-PC::HYPS -- (macro)

### ACL2-PC::ILLEGAL -- (macro)

### ACL2-PC::IN-THEORY -- (primitive)

### ACL2-PC::INDUCT -- (atomic macro)

### ACL2-PC::LISP -- (meta)

### ACL2-PC::MORE -- (macro)

### ACL2-PC::MORE! -- (macro)

### ACL2-PC::NEGATE -- (macro)

### ACL2-PC::NIL -- (macro)

`control-d`

### ACL2-PC::NOISE -- (meta)

### ACL2-PC::NX -- (atomic macro)

### ACL2-PC::ORELSE -- (macro)

### ACL2-PC::P -- (macro)

### ACL2-PC::P-TOP -- (macro)

### ACL2-PC::PP -- (macro)

### ACL2-PC::PRINT -- (macro)

### ACL2-PC::PRINT-ALL-GOALS -- (macro)

### ACL2-PC::PRINT-MAIN -- (macro)

### ACL2-PC::PRO -- (atomic macro)

### ACL2-PC::PROMOTE -- (primitive)

`implies`

term to top-level### ACL2-PC::PROTECT -- (macro)

### ACL2-PC::PROVE -- (primitive)

### ACL2-PC::PUT -- (macro)

### ACL2-PC::QUIET -- (meta)

### ACL2-PC::R -- (macro)

### ACL2-PC::REDUCE -- (atomic macro)

### ACL2-PC::REDUCE-BY-INDUCTION -- (macro)

### ACL2-PC::REMOVE-ABBREVIATIONS -- (primitive)

### ACL2-PC::REPEAT -- (macro)

### ACL2-PC::REPEAT-REC -- (macro)

`repeat`

### ACL2-PC::REPLAY -- (macro)

### ACL2-PC::RESTORE -- (meta)

### ACL2-PC::RETAIN -- (atomic macro)

**but**the indicated top-level hypotheses### ACL2-PC::RETRIEVE -- (macro)

### ACL2-PC::REWRITE -- (primitive)

### ACL2-PC::RUN-INSTR-ON-GOAL -- (macro)

### ACL2-PC::RUN-INSTR-ON-NEW-GOALS -- (macro)

`then`

### ACL2-PC::S -- (primitive)

### ACL2-PC::S-PROP -- (atomic macro)

### ACL2-PC::SAVE -- (macro)

### ACL2-PC::SEQUENCE -- (meta)

### ACL2-PC::SHOW-ABBREVIATIONS -- (macro)

### ACL2-PC::SHOW-REWRITES -- (macro)

### ACL2-PC::SKIP -- (macro)

### ACL2-PC::SL -- (atomic macro)

### ACL2-PC::SPLIT -- (atomic macro)

### ACL2-PC::SR -- (macro)

### ACL2-PC::SUCCEED -- (macro)

### ACL2-PC::TH -- (macro)

### ACL2-PC::THEN -- (macro)

### ACL2-PC::TOP -- (atomic macro)

### ACL2-PC::TYPE-ALIST -- (macro)

### ACL2-PC::UNDO -- (meta)

### ACL2-PC::UNSAVE -- (macro)

### ACL2-PC::UP -- (primitive)

### ACL2-PC::USE -- (atomic macro)

### ACL2-PC::X -- (atomic macro)

### ACL2-PC::X-DUMB -- (atomic macro)

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

### INSTRUCTIONS -- instructions to the proof checker

### MACRO-COMMAND -- compound command 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 have already been listed above.
Among them are proof-checker commands `help`

, `help-long`

, `more`

, and
`more!`

, which behave respectively like the ACL2 functions `:`

`doc`

,
`:`

`doc!`

, `:`

`more`

, and `:`

`more!`

.