next up previous contents index
Next: Showing GoalsSubgoals Up: The Proof Editor Previous: Motion within the

Initiating a Refinement

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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995