Next: Nuprl Terms
Up: Reference Material for Tutorial
Previous: Printing a Proof Tree
Useful LATEX-related unix shell commands are:
- 1.
- latex
file-name
to run LATEX on the .tex file
and generate a
file-name
.dvi file.
- 2.
- xdvi
file-name
to view the .dvi file on your screen.
- 3.
- dvips
file-name
| lpr -P
printer-name
to print the .dvi file.
Dora Abdullah, 12/4/97