The tool bar appears between the Command
and the State windows. It provides fast access
for very frequent commands and contains one check box and five buttons:
- The "Do it" Button.
This is the button to use to trigger the execution of a command that is
complete. There is more information on this command in the chapter about
script management.
- The "Automatic do it" Checkbox.
The Command window can be configured so that a command is sent to the proof
assistant as soon as it detects that this command does not contain any hole
anymore. This behavior is quite powerful and can be unsettling in certain
circumstances. This checkbox makes it possible to unplug this behavior. An
alternative is type <CTRL>T while the mouse is in the Commands,
the State or the Theorems window. The "Auto"
keyword that appears on the left is only an explanation, it is not active.
- The goal counter. the signs "<"
and ">" are button that can be clicked on to change the rank of the
current goal in the list of goals, when there are goals in the
State window. The two numbers in the middle
indicate the rank of the current goal and the number of goals.
- The Discard button. This button
can be used to provoke the undoing of the last executed command. There is more
information on this command in the chapter about
script management..
- The Abort button. This button can be
used to provoke the undoing of all the commands related to the ongoing proof.
There is more information on this command in the chapter about
script management..
The tool bar can be moved up and down by clicking on the grey areas that
surround it and dragging the mouse with the button still depressed. It is thus
possible to adjust the respective size of the three main panes of the CtCoq
window.