1signature Hol_pp =
2sig
3  type hol_type = Type.hol_type
4  type term     = Term.term
5  type thm      = Thm.thm
6  type theory   = DB.theory
7  type data     = DB.data
8  type 'a pprinter = 'a Parse.pprinter
9
10
11  val pp_type        : hol_type pprinter
12  val pp_term        : term pprinter
13  val pp_thm         : thm pprinter
14  val pp_theory      : theory pprinter
15
16  val type_to_string : hol_type -> string
17  val term_to_string : term -> string
18  val thm_to_string  : thm -> string
19
20  val print_type     : hol_type -> unit
21  val print_term     : term -> unit
22  val print_thm      : thm -> unit
23
24  val print_theory : string -> unit
25
26  val data_list_to_string : data list -> string
27  val print_apropos       : term -> unit
28  val print_find          : string -> unit
29  val print_match         : string list -> term -> unit
30
31  val print_theory_to_file      : string -> string -> unit
32  val print_theory_to_outstream : string -> TextIO.outstream -> unit
33  val export_theory_as_docfiles : string -> unit
34
35  val pp_theory_as_html         : string pprinter
36  val print_theory_as_html      : string -> string -> unit
37  val html_theory               : string -> unit
38
39end
40