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