Printing a Proof Tree

The proof editor only allows you to see a small section of a proof at a time, but you can also create a L^ATEX file which contain printed representation of a whole proof tree or sub-tree.

First move a proof editor window such that the goal in the proof window is either at the root of the whole proof or at some sub-tree you want to print. Then enter $\langle$C-T$\rangle$. A term-editor window called a transformation tactic window opens up, which should look like:

Transformation tactics are tactics which transform a whole proof tree. The tactics you have encountered so far are all refinement tactics which only work on the leaves of a proof tree. The transformation tactic you run to print a proof works by side-effect; it doesn't change the proof in any way. Enter:

Here, $\langle$file-name$\rangle$ should include a full pathname, and should not include an extension.

Enter $\langle$C-Z$\rangle$ to run the print tactic and exit the transformation tactic window. Two files are created: the L^ATEX file $\langle$file-name$\rangle$.tex and the file $\langle$file-name$\rangle$ .prl which can be viewed using emacs running with a nuprl font,