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
:Stop-proof-tree causes proof tree display to be
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.