IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
This editor is designed to edit entire proofs as terms. For advice on editing proof terms, see ProofEditing. Here is a sample proof term, which includes an unproved leaf.
1. A : Prop 2. B : Prop 3. C : Prop (A B C) (A & B C) by Analyze \ (A B C) A & B C by UnivCD ...w 4. A B C 5. A & B C by Analyze5 6. A 7. B " C by BackThru: Hyp:4 \ A by Auto --- B by Auto --- (A B C) (A & B C) by UnivCD ...w 4. A & B C 5. A 6. B C by <Unproved PREMISE>
For each assertion of the proof, the proofs of its subgoals is listed beneath it. If there is only one, it is just listed below in line. If there are more than one then they are shown like this:
Goal of proof by Tactic code for generating subgoals \ Proof of subgoal 1 --- Proof of subgoal 2 --- Proof of subgoal 3
(A 
B 
