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