CHECKPOINT-FORCED-GOALS

Cause forcing goals to be checkpointed in proof trees
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).