(continued from doc for pfterms)

It is suggested that you try these commands on the sample proof in doc for pfterms.

The units of assertion are called "sequents" and consist of a "conclusion" and possibly some "hypotheses" or "declarations".

1. A : Prop
2. B : Prop
3. C : Prop
4. A  B  C
5. A & B
  C

This sequent has conclusion C, three declarations (of variables A, B, and C), and two hypotheses, A  B  C and A & B.

To save space and reduce complexity for the user, hypotheses inherited by a subgoal from its parent are normally elided. In some methods of display, the conclusion is elided too if it's inherited.

Sometimes a section of the proof will be elided and displayed as ***; `(mouseleft)' will reveal the elided term.

To zoom in on a subproof, use `(mouseright)' on some part of the proof specific text of the goal you want to focus on (as opposed to the conclusion or hypotheses themselves). To zoom back out you may `(mouseright)' on the entire visible proof term, or the highest goal.

When you zoom in on a subproof, the address of that subproof is revealed, and looks like "top 1 2 1 1" indicating the path down from the top goal. If the point is located on or within a proof term, then `(mouseleft)' on "top" or one of these digits will navigate to the node at that proof address. (Thanks to Pavel Naumov for this idea.) This works even if the point is in one window, and the address notation is in another. This helps coordinate navigation when one has two copies of a proof.

When `show' or `(cm-(mouseright))' is used on proof term step, the tactic will be analyzed into simpler tactics or even primitive rules, and run in a new window.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html