GENERAL_REWRITE_CONV : bool -> (conv -> conv) -> gconv net -> thm list -> conv
Rewrite with theorems as well as an existing net.
The call GENERAL_REWRITE_CONV b cnvl net thl will regard thl as rewrite
rules, and if b = true, also potentially as conditional rewrite rules. These
extra rules will be incorporated into the existing net, and rewriting applied
with a search strategy cnvl (e.g. DEPTH_CONV).
This is mostly for internal use, but it can sometimes be more efficient when
rewriting with large sets of theorems repeatedly if they are first composed
into a net and then augmented like this.
- SEE ALSO