print_theory_as_tex : string -> unit
Emits a theory as LaTeX commands.
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.

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.
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
Some examples of the available LaTeX commands are listed below:
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:

The date the theory was build can be displayed with:
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,

can be used inside tables and figures.
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
However, note that this will adversely effect the alignment of the output.
HOL  Kananaskis-13