start displaying proof trees during proofs
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 :stop-proof-tree.

Do not attempt to invoke start-proof-tree during an interrupt in the middle of a proof.