Structure hhExportTh1


Source File Identifier index Theory binding index

signature hhExportTh1 =
sig

include Abbrev

  type thmid = string * string
  val th1_write_pb : string -> (thmid * (string list * thmid list)) -> unit
  val th1_export_bushy : string -> string list -> unit
  val th1_export_chainy : string -> string list -> unit

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1