1signature ThmSetData =
2sig
3
4  type data = Theory.LoadableThyData.t
5  type thm = Thm.thm
6  type thname = KernelSig.kernelname
7  datatype setdelta = ADD of thname * thm | REMOVE of string
8  type exportfns =
9       { add : {thy : string, named_thm : thname * thm} -> unit,
10         remove : {thy : string, remove : string} -> unit}
11  val added_thms : setdelta list -> thm list
12  val mk_add : string -> setdelta
13
14  val new_exporter :
15      {settype : string, efns : exportfns} ->
16      {export : string -> unit, delete : string -> unit}
17
18  val current_data : {settype:string} -> setdelta list
19  val theory_data : {settype : string, thy: string} -> setdelta list
20  val all_data : {settype:string} -> (string * setdelta list) list
21  val data_exportfns : {settype:string} -> exportfns option
22
23  val all_set_types : unit -> string list
24
25  type 'value ops = {apply_to_global : setdelta -> 'value -> 'value,
26                     thy_finaliser : ({thyname:string} -> setdelta list ->
27                                      'value -> 'value) option,
28                     uptodate_delta : setdelta -> bool, initial_value : 'value,
29                     apply_delta : setdelta -> 'value -> 'value}
30  val export_with_ancestry:
31      {settype : string, delta_ops : 'value ops} ->
32      (setdelta,'value) AncestryData.fullresult
33
34end
35