next up previous contents
Next: Creating a Theorem Up: Theories Previous: Loading an Existing Theory

Printing a Theory

 Print a loaded theory using:





\begin{parbox} {25em} {\tt print\_theory {\tt \char `\uml }{}user{}{\tt \char `\... ...hbox{ \framebox {\rule[-.2ex]{0em}{1.5ex}\sc return} }\hspace{.2em}}\end{parbox}




If $\langle$file-name$\rangle$ is the file-name associated with your user theory, then two files are generated; a text file $\langle$file-name$\rangle$.prl and a self-contained LATEX file $\langle$file-name$\rangle$.tex.


Dora Abdullah, 12/4/97