(checkpoint-forced-goals)
t) has been executed. To return to the default behavior, use the
command (checkpoint-forced-goals nil).
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 in the documentation for 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).