verify),
use help to get a list of legal instructions and (help instr)
to get help for the instruction instr.
Major Section: PROOF-CHECKER
Example:
:instructions (induct prove promote (dive 1) x
(dive 2) = top (drop 2) prove)
See defthm for the role of :instructions in place of
:hints. As illustrated by the example above, the value
associated with :instructions is a list of proof-checker
commands. At the moment the best way to understand the idea of the
interactive proof-checker (see proof-checker and
see verify) is probably to read the first 11 pages of CLI
Technical Report 19, which describes the corresponding facility for
Nqthm.
When inside the interactive loop (i.e., after executing verify),
use help to get a list of legal instructions and (help instr)
to get help for the instruction instr.