1signature ThmSetData =
2sig
3
4  type data = Theory.LoadableThyData.t
5  val new_exporter : string ->
6                     (string -> (string * Thm.thm) list -> unit) ->
7                     {dest : data -> (string * Thm.thm) list option,
8                      export : string -> unit,
9                      mk : string list -> data * (string * Thm.thm) list}
10
11  val new_storage_attribute : string -> unit
12  val store_attribute : {attribute: string, thm_name : string} -> unit
13
14  val current_data : string -> (string * Thm.thm) list
15  val theory_data : {settype : string, thy: string} ->
16                    (string * Thm.thm) list
17  val all_data : string -> (string * (string * Thm.thm) list) list
18  val data_storefn : string -> (string -> unit) option
19  val data_exportfn :
20      string -> (string -> (string * Thm.thm) list -> unit) option
21
22  val all_set_types : unit -> string list
23
24end
25