next up previous contents
Next: Nuprl Terms Up: Reference Material for Tutorial Previous: Printing a Proof Tree

Running LATEX

Useful LATEX-related unix shell commands are:

1.
latex $\langle$file-name$\rangle$
to run LATEX on the .tex file and generate a $\langle$file-name$\rangle$.dvi file.

2.
xdvi $\langle$file-name$\rangle$
to view the .dvi file on your screen.

3.
dvips $\langle$file-name$\rangle$ | lpr -P$\langle$printer-name$\rangle$
to print the .dvi file.


Dora Abdullah, 12/4/97