print_term_as_tex : term -> unit
STRUCTURE
EmitTeX
SYNOPSIS
Prints a term as LaTeX.
DESCRIPTION
An invocation of print_term_as_tex tm will print the term tm, replacing various character patterns (e.g. /\ and \/) with LaTeX commands. The translation is controlled by the string to string function EmitTeX.hol_to_tex.
FAILURE
Should never fail.
EXAMPLE
 - EmitTeX.print_term_as_tex ``\l h. {x | l <= x /\ x <= h}`` before print "\n";
 \HOLTokenLambda{}l h. \HOLTokenLeftbrace{}x | l \HOLTokenLeq{} x \HOLTokenConj{} x \HOLTokenLeq{} h\HOLTokenRightbrace{}
 > 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_type_as_tex, print_theorem_as_tex, print_theory_as_tex, print_theories_as_tex_doc, tex_theory
HOL  Trindemossen-1