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