1signature ThyDataSexp = 2sig 3 4datatype t = 5 Int of int 6 | String of string 7 | List of t list 8 | Term of Term.term 9 | Type of Type.hol_type 10 | Thm of Thm.thm 11 | Sym of string 12 | Bool of bool 13 | Char of char 14 | Option of t option 15 16val uptodate : t -> bool 17val compare : t * t -> order 18 19(* note that merge functions must take identical "types" on both sides. 20 Thus, if the theory data is a list of values, both old and new should be 21 lists and the merge will effectively be an append. If there's just one 22 value being "merged", it should still be a singleton list. 23 24 Similarly, if the data is a dictionary, represented as an alist, then the 25 new data (representing a single key-value maplet) should be a singleton 26 alist 27*) 28val alist_merge : {old: t, new : t} -> t 29val append_merge : {old : t, new : t} -> t 30 31val new : {thydataty : string, 32 merge : {old : t, new : t} -> t, 33 load : {thyname : string, data : t} -> unit, 34 other_tds : t * TheoryDelta.t -> t} -> 35 {export : t -> unit, segment_data : {thyname : string} -> t option} 36 37val pp_sexp : Type.hol_type PP.pprinter -> Term.term PP.pprinter -> 38 Thm.thm PP.pprinter -> t PP.pprinter 39 40end 41