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