Structure DiskThms

Source File	Identifier index	Theory binding index

signature DiskThms =
sig

  val ppwrite : PP.ppstream -> (string * Thm.thm) list -> unit
  val write_stream : TextIO.outstream -> (string * Thm.thm) list -> unit
  val write_file : string -> (string * Thm.thm) list -> unit
  val read_stream : TextIO.instream -> (string * Thm.thm) list
  val read_file : string -> (string * Thm.thm) list

end

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-10