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".