Next: Constructive and Classical
Up: Tactics
Previous: Autotactics
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 (a:tok)
-
-
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.
Karla Consroe
Wed Oct 23 13:48:45 EDT 1996