Figure: A Proof Window on a New Proof
When a new proof window is opened, the window appears as in
Figure 
. By using SELECT with the cursor
over <main proof goal> a term window is opened up to allow one
to enter the main goal of the proof.
One can also use SELECTSELECT on the main goals of incomplete or
complete proofs. For example, one might want to copy the main goal of
one theorem and use it as the basis for the main goal of another, or
one might want to correct a mis-stated main goal. Note however that
if a main goal is destructively modified and checked
, then any
existing proof is lost. As explained in
Section , the window is checked
whenever the EXITEXIT term window command is used. If the window is
not modified but checked, or modified and then quitted, then any
existing proof will not be changed. Warning: a window counts as being
modified even if changes have been made and then undone, so it
looks the same as it originally was.