Transformation Tactics

PrintTexFile (name:string)

name should be a filename without extension. Two files are created. name.prl is a file which can be viewed by an appropriate version of emacs running with one of Nuprl's 8-bit fonts.  name.tex is a self-contained file suitable for input to LaTeX.

Mark (a:tok)

Mark stores the proof tree at and below the point in the proof where it is invoked in the proof register named a.

Restore  the proof stored in proof register a by a previous Mark.

Copy (a:tok)

Run all the tactics associated with the proof stored in proof register a. Copy is useful if you want to copy a pattern of reasoning used in one part of a proof to another part. Copy  can also be used to copy  from one proof to another.

Z

Stores the current proof in the ML variable pf. This is very useful when debugging tactics.