add_rewrites : rewrites -> thm list -> rewrites
SYNOPSIS
Add theorems to a collection of rewrite rules.
LIBRARY
bool
STRUCTURE
Rewrite
DESCRIPTION
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
bool_rewrites, empty_rewrites, implicit_rewrites, GEN_REWRITE_CONV, GEN_REWRITE_RULE, GEN_REWRITE_TAC
HOL  Trindemossen-1