1signature DiskThms =
2sig
3
4  val ppwrite : (string * Thm.thm) list Parse.pprinter
5  val write_stream : TextIO.outstream -> (string * Thm.thm) list -> unit
6  val write_file : string -> (string * Thm.thm) list -> unit
7  val read_stream : TextIO.instream -> (string * Thm.thm) list
8  val read_file : string -> (string * Thm.thm) list
9
10end
11