The proof editor is designed principally to support the `top-down' refinement style generation of proofs. The refinement style entails repeatedly choosing an unrefined leaf node of a proof and a rule (usually a tactic) to try on that node. If the rule applies, the Nuprl system changes the node to a refined node, and automatically generates appropriate children nodes.
The editor also supports the application of transformation tactics
to proofs. These are usually applied to already refined nodes
of a proof tree and either change the structure of the proof they are
applied to or have some side effect. Transformation tactics are described
in Section 
.
The proof editor generates windows onto sections of proofs. One can have windows open on different proofs at the same time, and even multiple windows onto the same proof. In the latter event, the windows become `read-only'.
Proofs associated with theorem objects are not first copied when they are viewed with the proof editor, so all changes made to proofs take effect immediately. This is in contrast to the situation with the term editor where changes are only committed when you exit an object or ask for changes to be explicitly saved. If you want to make tentative changes to a section of a proof, you can use the Mark transformation tactic to first make a good copy of that section, or you can make a copy of the whole theorem object.