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