A refinement rule window is opened whenever the SELECT COMMAND
is used with the proof cursor over the rule place-holder. (For
example see Figure 
) The window always
has the title EDIT rule of theorem where theorem is
the name of the library object holding the proof. A new refinement
rule window is always initialized to allow one to type in an ML
tactic. The structure and special editing commands for this term
window are the same as for ML objects.
Soon, it will be possible to initialize
the refinement rule window to hold other kinds of rules (For example a
primitive rule). We will describe special term editor support for
these options here. Most users will only use tactics in refinement
rule windows. After a rule has been keyed in, and the term window
EXIT command has been given, Nuprl
parses the rule and tries to
apply it to the goal of the current proof. If the rule succeeds the
proof window is 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, Nuprl
will display some diagnostic
message and leave the rule window on the
screen so that it can be fixed.
One can also use SELECT on existing refinement rules.
For example, one might want to copy one rule in order to use
it as the basis of another or one might want to change the rule.
If a refinement rule is destructively modified
and checked,
then any existing subproofs below the rule are lost. As explained in
Section , the window is checked
whenever the EXIT 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.