To refine a goal, a refinement rule must be supplied.
To do this, first move the cursor to point to the rule of the current node
and press SEL
;
this will bring up an instance of the text editor in a window labeled
EDIT rule of thmname.
Type the rule into this window and press 
.
will parse the rule and try to apply it to the goal of the current proof tree node. If it succeeds the proof window will be redrawn with new statuses and subgoals as necessary. If it fails then one of two things may happen. If the error is severe, the status of the node (and the proof) will be set to bad, an error message will appear in the command/status window, and the rule will be set to ??bad refinement rule??. If the error is mild and due to a missing input,
will display a HELP message in the command/status window and leave the rule window on the screen so that it can be fixed.
If an existing rule is selected for editing
will copy it to the edit
window.
If the text of the rule is changed, then when 
is pressed
will again parse and refine the current goal.
When it does it will throw away any proofs for the children of the current
node,
even if they could have been applied to the new children of the
current node.
On the other hand, if the text is not changed, then when 
is pressed
will not reparse the rule.