print_theory_as_tex : string -> unit
STRUCTURE
EmitTeX
SYNOPSIS
Emits a theory as LaTeX commands.
DESCRIPTION
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
print_term_as_tex, print_type_as_tex, print_theorem_as_tex, print_theories_as_tex_doc, tex_theory
HOL  Trindemossen-1