print_theorem_as_tex : thm -> unit
STRUCTURE
EmitTeX
SYNOPSIS
Prints a theorem as LaTeX.
DESCRIPTION
An invocation of print_theorem_as_tex thm will print the term thm, replacing various character patterns (e.g. /\ and \/) with LaTeX commands. The translation is controlled by the string to string function EmitTeX.hol_to_tex. If the theorem is for a datatype then the function datatype_thm_to_string is used to produce the orginal declaration.
FAILURE
Should never fail.
EXAMPLE
 - EmitTeX.print_theorem_as_tex listTheory.CONS before print "\n";
 \HOLTokenTurnstile{} \HOLTokenForall{}l. \HOLTokenNeg{}NULL l \HOLTokenImp{} (HD l::TL l = l)
 > val it = () : unit
 - EmitTeX.print_theorem_as_tex listTheory.datatype_list before print "\n";
 list = [] | CONS of \HOLTokenQuote{}a \HOLTokenImp{} \HOLTokenQuote{}a list
 > val it = () : unit
COMMENTS
The LaTeX style file holtexbasic.sty (or holtex.sty) should be used and the output should be pasted into a Verbatim environment.
SEEALSO
print_term_as_tex, print_type_as_tex, print_theory_as_tex, print_theories_as_tex_doc, tex_theory
HOL  Trindemossen-1