1signature ThmAttribute = 2sig 3 4 type attrfun = {name:string,attrname:string,thm:Thm.thm} -> unit 5 type attrfuns = {localf : attrfun, storedf : attrfun} 6 val register_attribute : string * attrfuns -> unit 7 8 val store_at_attribute : attrfun 9 val local_attribute : attrfun 10 val extract_attributes : string -> string * string list 11 12 13end 14