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