| | | B.4.6 goal: Make Formula Goal |
goal F
In proving mode.
The command takes the label F of an assumption in the current proof state. It generates a single child state where the formula has been removed from the assumptions and the negated version of the formula becomes the single goal; the negated versions of the original goals become additional assumptions. The command thus implements the rule
[E] ..._1, ..._2, ~..._3 |- ~A
------------------------------
[E] ..._1, A, ..._2 |- ..._3
Some commands, especially the commands scatter and split, treat the goal of a proof states specially in that they attempt to split goal formulas (but not assumptions). By application of the command goal, one may make the right formula the target of splitting in a subsequent application of scatter or split.
| | | B.4.6 goal: Make Formula Goal |