instructions to the proof checker
Major Section:  PROOF-CHECKER

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