More on Making Proof Steps. (See also PF and TacMenu1 for more handy devices.)

Mini-menu for tactics.

Besides Auto the most common tactics can be invoked with `(mouseleft)' clicked on the turnstile or hyp number within a goal. This will insert a little menu at the point of tactics pertinent to that hyp or conclusion. Actually, if the point is an empty slot, usually within the tactic code part of a proof, the clause number will be inserted, and you must click again on the same hyp or turnstile to get the menu inserted at the point.

Kreitzing. `kr' `{(c-n)(m-n)}kr'

It often happens that after you have built several inference steps, you find them too fine-grained and wish that all the steps were compacted into one. If you locate the point on the subproof you wand to treat as a single step, the command `kr' will compose all the tactic code for the subproof into a single tactic and re-execute.

This conversion is called "Kreitzing" after Christoph Kreitz, who was the first to employ such compression systematically.

There is also a heuristic for undoing kreitzed code, which is invoked by `{(c-n)(m-n)}kr'.

Rerunning Proofs. `run'

The subgoals of a legitimate Nuprl proof are always determined by the goal and the tactic code. This means that a proof can be completely recreated from the top goal and the tree of tactic code gleaned from the proof tree. If one takes a proof and modifies it, say by changing the goal or perhaps some of the internal tactics, rather tan rebuilding the analogous proof step-by-step, one can simply rerun the proof from the goal down, regenerating the subproofs.

The `run' command will do this. If for some reason the proof cannot be run below a certain point in the proof, say because some tactic fails or the number of subgoals is not as expected, an error message is inserted at that point and no further progress down THAT subproof is attempted.

The user may then attempt to make repairs at that point or perhaps higher, then rerun the proof from the corrected point down.

Copying one inference on top of another.

When an inference step term, B, is copied on top of another, A, say with the `(m-(mouseright))' command, the goal and address of A are kept, but the tactic code and subproofs are taken from B. If the goals are different, then the new step will be rerun as with `run' above.