\DOC

\TYPE {print_theories_as_tex_doc : string list -> string -> unit}

\SYNOPSIS
Emits theories as LaTeX commands and creates a document template.

\DESCRIBE

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
}

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

\ENDDOC