IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
When an operator definition or declaration, an ABS object, is "verified" with the `(c-v)' command, the editor checks the existence and contents of various related objects for coherency with the ABS object, and may raise a utility for modifying or adding related objects such as display form specs (DISPs), well-formedness theorems (THMs), and "pseudo-step" specifications which are mainly to expand recursively defined operators.
For a newly defined operator, the utility has buttons for defining a new display form and, normally, a new well-formedness lemma.
If your definition is recursive, you should allow the pseudo-step spec to be created.
If you change a definition, you will get a number of buttons for updating the auxilliary objects.
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html