tex_theory
EmitTeX.tex_theory : string -> unit
Emits theory as LaTeX commands and creates a document template.
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".
See also
EmitTeX.print_term_as_tex,
EmitTeX.print_type_as_tex,
EmitTeX.print_theorem_as_tex,
EmitTeX.print_theory_as_tex,
EmitTeX.print_theories_as_tex_doc