Start-proof-tree
Start displaying proof trees during proofs
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 may be found elsewhere: see proof-tree. In a nutshell: :start-proof-tree causes proof tree display
to be turned on, once it has been turned off by :stop-proof-tree.
Do not attempt to invoke start-proof-tree during an interrupt in the
middle of a proof.