| | | B.3 Primary Commands |
This section lists the commands typically applied in the initial phase of decomposing a proof into simple proof states (scatter, decompose, split, possibly induction) and in the final phases of closing proof states (autostar, auto). In the middle proof phases, typically the commands in the next section are applied.
| | | B.3 Primary Commands |