print_theories_as_tex_doc

EmitTeX.print_theories_as_tex_doc : string list -> string -> unit

Emits theories as LaTeX commands and creates a document template.

An invocation of print_theories_as_tex_doc thys name will export the named theories thys as a collection of LaTeX commands and it will also generate a document, whose file name is given by name, that presents all of the theories. The theories are 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, the theories may be overwritten.

Example

The invocation

 - EmitTeX.print_theories_as_tex_doc ["arithmetic", "list", "words"] "report";
 > val it = () : unit

will generate four files “HOLarithmetic.tex”, “HOLlist.tex”, “HOLwords.tex” and “report.tex”.

The document can be built as follows:

 $ cp $HOLHOME/src/emit/holtex.sty .
 $ pdflatex report
 $ makeindex report
 $ pdflatex report

See also

EmitTeX.print_term_as_tex, EmitTeX.print_type_as_tex, EmitTeX.print_theorem_as_tex, EmitTeX.print_theory_as_tex, EmitTeX.tex_theory