Next: Selecting, Previous: Connectives, Up: Basic Usage

### 4.3 Adding Sentences

Hitting `Ctrl+J` adds a conclusion to the proof. A conlusion is always added after the current line, or, if the line is a premise, then the conclusion is added after the last premise. If the current line is a conclusion, then it is highlighted in cyan.

Hitting `Ctrl+P` adds a premise to the proof. A premise will always be added after the last premise.

Pressing `Ctrl+B` adds a subproof to the proof. When in a subproof, a conclusion will always be added within the subproof. The first line of a subproof does not require a rule, but instead acts as a premise. Pressing `Ctrl+D` ends the current subproof. This creates a new conclusion just after the subproof.

To undo a command, simply press `Ctrl+Z`. This will undo the last text modification, insertion, or deletion. In the case of several insertions or several deletions, undo will undo all of them. To undo an undo, press `Ctrl+Y`, or redo.