1signature hhWriter =
2sig
3
4  include Abbrev
5
6  val write_thyl       :
7    string ->
8    (string -> (string * thm) * string -> bool) ->
9    string list ->
10    unit
11  val write_problem    :
12    string ->
13    (string -> (string * thm) * string -> bool) ->
14    (string * thm) list ->
15    string list ->
16    term ->
17    unit
18
19  val write_thydep     : string -> string list -> unit
20  val reserved_names   : string list
21
22end
23