----------------------------------------------------------------------
print_theory_as_tex                                          (EmitTeX)
----------------------------------------------------------------------
print_theory_as_tex : string -> unit

SYNOPSIS
Emits a theory as LaTeX commands.

DESCRIBE
An invocation of {print_theory_as_tex thy} will export the named theory
as a collection of LaTeX commands.  The output file is named
"HOLthy.tex", where {thy} is the named theory.  The prefix "HOL" can be
changed by setting {holPrefix}.  The file is stored in the
directory {emitTeXDir}. By default the current working directory is used.

The LaTeX file will contain commands for displaying the theory’s datatypes,
definitions and theorems.

FAILURE
Will fail if there is a system error when trying to write the file.  If the theory is not loaded then a message will be printed and an empty file will be created.

EXAMPLE
The list theory is exported with:

 - EmitTeX.print_theory_as_tex "list";
 > val it = () : unit

The resulting file can be included in a LaTeX document with

 \input{HOLlist}

Some examples of the available LaTeX commands are listed below:

 \HOLlistDatatypeslist
 \HOLlistDefinitionsALLXXDISTINCT
 \HOLlistTheoremsALLXXDISTINCTXXFILTER

Underscores in HOL names are replaced by "XX"; quotes become "YY" and numerals are expanded out e.g. "1" becomes "One".

Complete listings of the datatypes, definitions and theorems are displayed with:

 \HOLlistDatatypes
 \HOLlistDefinitions
 \HOLlistTheorems

The date the theory was build can be displayed with:

 \HOLlistDate

The generated LaTeX will reflect the output of {Parse.thm_to_string}, which
is under the control of the user.  For example, the line width can be changed
by setting {Globals.linewidth}.

The Verbatim display environment is used, however, "boxed" versions can be
constructed.  For example,

 \BUseVerbatim{HOLlistDatatypeslist}

can be used inside tables and figures.

COMMENTS
The LaTeX style file {holtexbasic.sty} (or {holtex.sty}) should be used.  These style files can be modified by the user.  For example, the font can be changed to Helvetica with

 \fvset{fontfamily=helvetica}

However, note that this will adversely effect the alignment of the output.

SEEALSO
EmitTeX.print_term_as_tex, EmitTeX.print_type_as_tex,
EmitTeX.print_theorem_as_tex, EmitTeX.print_theories_as_tex_doc,
EmitTeX.tex_theory.

----------------------------------------------------------------------