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