`(c-z)'

The most common procedure for building a proof step is to fill in the tactic-code part of an inference step form with ML Code then issuing the generic execution command `(c-z)'. `(c-z)' will jump up to the smallest proof step containing the highlighted point, and "refine" the goal to produce subgoals.
Note: Whatever subproofs may already be there will be replaced by the new subgoals, if any. Non-trivial subproofs that are discarded will be popped up in another window so you get another crack at using them, say for cut-n-paste.
If you know you don't want these subproofs, delete them before using `(c-z)'. To delete them, locate the point on the group of subgoals as a group then use `(c-d)'; you don't need to move the point back to use `(c-z)'. The `(mousemiddle)' command is most useful for moving the point to a large term -- play with it.

The Auto Tactic.

Many simple inferences are knocked off by the tactic Auto. It is so common to try it, that the `(c-z)' command has been tailored to insert it automatically in some circumstances. If there are no subproofs, and the tactic code slot is empty, then `(c-z)' will insert Auto and execute.
There are three common variants of the auto tactic: Auto Auto' SIAuto
`(backspace)' will cycle among them. (No explanation given at this point.)

Subgoals are often labeled "wf" for well-formedness goals, which assert that expressions have certain types. Often Auto will be useful on these subgoals even when it may be worse than useless on other sugoals. When this is the case, we don't want use (T ....), but instead we want a variant (T ...w) that applies Auto after T only to the well-formedness subgoals. The command `{auauto}w' will append Auto this way.

See EXAMPLE for an exercise using these methods.

doc for proof refinement2 IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html