Major Section: PROOF-TREE
Also see proof-tree and see start-proof-tree. Note that
:stop-proof-tree
works by adding '
proof-tree
to the
inhibit-output-lst
; see set-inhibit-output-lst.
Proof tree displays are explained in the documentation for proof-tree.
:Stop-proof-tree
causes proof tree display to be turned off.
It is permissible to submit the form (stop-proof-tree)
during a break.
Thus, you can actually turn off proof tree display in the middle of a proof
by interrupting ACL2 and submitting the form (stop-proof-tree)
in raw
Lisp.