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