Major Section: PROOF-TREE
Example forms: (checkpoint-forced-goals t) (checkpoint-forced-goals nil)Also see proof-tree.
By default, goals are not marked as checkpoints by a proof tree display (as
described elsewhere; see proof-tree) merely because they force some
hypotheses, thus possibly contributing to a forcing round. However, some
users may want such behavior, which will occur once the command
(checkpoint-forced-goals t) has been executed. To return to the
default behavior, use the command (checkpoint-forced-goals nil).
