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