Next: Rules Table, Up: Menu Options

### 5.1 Proof Windows

These are the menu options for the main proof windows. Each one can be assigned a key command.

‘`New`’
‘`Ctrl+N`’
  Start a new proof. A new window is opened for this proof.
‘`Open`’
`CTRL+O`
  Open an existing proof in a new window.
‘`Save`’
`CTRL+S`
  Save the current proof.
‘`Save As`’
`CTRL+SHIFT+S`
  Save the current proof under a different name.
‘`Export to LaTeX...`’
  Export the current proof to a LaTeX file.
‘`Close`’
`CTRL+W`
  Close the current proof.
‘`Quit`’
`CTRL+Q`
  Exit Aris. But since logic is so much fun, I doubt you'll ever want to use this one.
‘`Add Premise`’
`CTRL+P`
  Insert a new premise at the end of the other premises.
‘`Add Conclusion`’
`CTRL+J`
  Insert a new conclusion after the current line if it is a conclusion, or at the start of the conclusions if it is a premise.
‘`Add Subproof`’
`CTRL+B`
  Begin a new subproof after the current line if it is a conclusion, or at the start of the conclusions if it is a premise. This is unavailable in boolean mode, since subproofs can't be used.
‘`End Subproof`’
`CTRL+D`
  End the current subproof, if there is one. Otherwise, this doesn't do anything. This is unavailable in boolean mode, since subproofs can't be used.
‘`Undo`’
`CTRL+Z`
  Undo the last modification to the current proof. On a new file, this does nothing.
‘`Redo`’
`CTRL+Y`
  Undo an undo operation. If no undo has been made, then this does nothing.
‘`Copy Line`’
`CTRL+G`
  Copy the current line.
‘`Kill Line`’
`CTRL+K`
  Kill, or cut, the current line. This removes the line from the proof.
‘`Insert Line`’
`CTRL+I`
  Insert the copied/killed line.
‘`Evaluate Line`’
`CTRL+E`
  Evaluate the logical validity of the current line.
‘`Evaluate Proof`’
`CTRL+F`
  Evaluate the logical validity of the current proof. This evaluates each line of the proof.
‘`Toggle Goals...`’
`CTRL+L`
  Toggle the goal window for the current proof.
‘`Toggle Boolean Mode`’
`CTRL+M`
  Toggle boolean mode for the current proof See Boolean Rules.
‘`Import Proof`’
  Import another proof into this one. This will merge the premises of the other proof into the current one, and insert the goals of the other proof as conclusions. In addition, it sets the conclusions' references as the premises, and sets them all to use the lemma rule see lm.
‘`Toggle Rules`’
`CTRL+R`
  Toggle the rules window.
‘`Small`’
`CTRL+-`
  Change the font size to small (8pt).
‘`Medium`’
`CTRL+0`
  Change the font size to medium (12pt).
‘`Large`’
`CTRL+=`
  Change the font size to large (16pt).
‘`Custom`’
  Change the font size to a custom size. This menu option opens a dialog box with a numerical entry.
‘`Contents`’
`F1`
  Display Aris help. This is the only key command that cannot be modified.
‘`About GNU Aris`’
  Displays information about GNU Aris.