tex_theory : string -> unit
STRUCTURE
SYNOPSIS
Emits theory as LaTeX commands and creates a document template.
DESCRIPTION
An invocation of tex_theory thy will export the named theory thy as a collection of LaTeX commands and it will also generate a document "thy.tex" that presents the theory. The string "-" may be used to denote the current theory segment. The theory is exported with print_theory_as_tex.
FAILURE
Will fail if there is a system error when trying to write the files. It will not overwite the file name, however, "HOLname.tex" may be overwritten.
EXAMPLE
The invocation
 - EmitTeX.tex_theory "list";
 > val it = () : unit
will generate two files "HOLlist.tex" and "list.tex".

SEEALSO
HOL  Trindemossen-1