1signature EmitTeX =
2sig
3    include Abbrev
4
5    val texLinewidth              : int ref
6    val texPrefix                 : string ref
7    val emitTeXDir                : string ref
8
9    val non_type_definitions      : string -> (string * thm) list
10    val non_type_theorems         : string -> (string * thm) list
11    val datatype_theorems         : string -> (string * thm) list
12    val print_datatypes           : string -> unit
13    val datatype_thm_to_string    : thm -> string
14
15    type override_map = string -> (string * int) option
16    val raw_pp_term_as_tex        : override_map -> term PP.pprinter
17    val raw_pp_type_as_tex        : override_map -> hol_type PP.pprinter
18    val raw_pp_theorem_as_tex     : override_map -> thm PP.pprinter
19
20    val pp_term_as_tex            : term PP.pprinter
21    val pp_type_as_tex            : hol_type PP.pprinter
22    val pp_theorem_as_tex         : thm PP.pprinter
23
24    val print_term_as_tex         : term -> unit
25    val print_type_as_tex         : hol_type -> unit
26    val print_theorem_as_tex      : thm -> unit
27    val print_theory_as_tex       : string -> unit
28
29    val print_theories_as_tex_doc : string list -> string -> unit
30
31    val tex_theory                : string -> unit
32end
33