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