For explanation of the term representation of proofs, see ProofTerms.

Proof terms may be as freely edited as any other terms, so you may cut-and-paste them together or build them explicitly without regard for validity. But of course, we normally use specific utilities to help us form proof terms that consist of actually legitimate inferences by executing a tactic at each step.

THM objects.

THM objects may contain only proofs in which every step is legitimate according to the basic rules of inference. See PostingTHMs for how to post theorems to the library, and so making them available for further use as lemmas.

Starting a proof.

If you initiate a proof by creating a new THM object, say with the NEW button in MainMenu, or view an existing THM object, You will be given a proof term which you may then modify.
If you want to build a proof from scratch, unmediated by a THM object, simply create a "mathematical" expression (i.e., not a WORDS document, nor ML Code, nor other special purpose system expression), then use the generic execution command `(c-z)'.
This will create a sequent with no hypotheses, perhaps inserting some universal quantifiers for variables you left free. You should edit this term until no free variables are left, for which purpose you will find the generic adjustment command `adj' useful.

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