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