----------------------------------------------------------------------
add_rewrites                                                 (Rewrite)
----------------------------------------------------------------------
add_rewrites : rewrites -> thm list -> rewrites

SYNOPSIS
Add theorems to a collection of rewrite rules.

KEYWORDS
rewriting, simplification

LIBRARY
bool

DESCRIBE
The function {add_rewrites} processes each element in a list of
theorems and adds the resulting rewrite rules to a value of type
{rewrites}.

FAILURE
Never fails.

EXAMPLE

- load "pairTheory"; open pairTheory;
  add_rewrites empty_rewrites (PAIR_MAP_THM::pair_rws);

> val it =
    |- (f ## g) (x,y) = (f x,g y);
    |- (FST x,SND x) = x;
    |- FST (x,y) = x;
    |- SND (x,y) = y
    Number of rewrite rules = 4
     : rewrites




USES
For building bespoke rewrite rule sets.

SEEALSO
Rewrite.bool_rewrites, Rewrite.empty_rewrites,
Rewrite.implicit_rewrites, Rewrite.GEN_REWRITE_CONV,
Rewrite.GEN_REWRITE_RULE, Rewrite.GEN_REWRITE_TAC.

----------------------------------------------------------------------