sig
  type rrules_set
  val new_rules_set :
    (bool * Term.term * Term.term) list -> Rewriting.rrules_set
  val add_first_rule :
    Rewriting.rrules_set ->
    bool * Term.term * Term.term -> Rewriting.rrules_set
  val add_last_rule :
    Rewriting.rrules_set ->
    bool * Term.term * Term.term -> Rewriting.rrules_set
  val merge_rules :
    Rewriting.rrules_set -> Rewriting.rrules_set -> Rewriting.rrules_set
  val empty_rrules : Rewriting.rrules_set -> bool
  val rewrite :
    Term.decls_set -> Rewriting.rrules_set -> Term.term -> Term.term
  val normalise_brackets : Term.term -> Term.term
  val normalise :
    Term.decls_set ->
    Term.term Term.TermHashtbl.t ->
    (string, Rewriting.rrules_set) Hashtbl.t ->
    (string -> bool) -> (Term.term -> Term.term) -> Term.term -> Term.term
end