add_rewrites
Rewrite.add_rewrites : rewrites -> thm list -> rewrites
Add theorems to a collection of rewrite rules.
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::pairLib.pair_rws);
val it = (): unit
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
For building bespoke rewrite rule sets.
See also
Rewrite.bool_rewrites,
Rewrite.empty_rewrites,
Rewrite.implicit_rewrites,
Rewrite.GEN_REWRITE_CONV,
Rewrite.GEN_REWRITE_RULE,
Rewrite.GEN_REWRITE_TAC