Major Section: PROOF-TREE
Also see proof-tree and see stop-proof-tree. Note that
:start-proof-tree works by removing
proof-tree from the
inhibit-output-lst; see set-inhibit-output-lst.
Explanations of proof tree displays, including emacs support, may be found
elsewhere; see proof-tree and see proof-tree-emacs. In a nutshell:
:start-proof-tree causes proof tree display to be turned on, once it has
been turned off by
Do not attempt to invoke
start-proof-tree during an interrupt in the
middle of a proof.