1signature simpfrag =
2sig
3
4  include Abbrev
5  type convdata = { name: string,
6                    key: (term list * term) option,
7                    trace: int,
8                    conv: (term list -> term -> thm) -> term list -> conv}
9
10  type simpfrag = { convs: convdata list, rewrs: thm list}
11
12  val empty_simpfrag : simpfrag
13  val add_rwts : simpfrag -> thm list -> simpfrag
14  val add_convs : convdata list -> simpfrag -> simpfrag
15
16  val register_simpfrag_conv : {name: string, code: thm -> convdata} -> unit
17  val lookup_simpfrag_conv : string -> (thm -> convdata) option
18  val simpfrag_conv_tag : string  (* used to mark TypeBase extra sexps *)
19
20end
21