REWRITES_CONV : ('a * (term -> 'b)) net -> term -> 'b

Apply a prioritized conversion net to the term at the top level.

The underlying machinery in rewriting and simplification assembles (conditional) rewrite rules and other conversions into a net, including a priority number so that, for example, pure rewrites get applied before conditional rewrites. If net is such a net (for example, constructed using mk_rewrites and net_of_thm), then REWRITES_CONV net is a conversion that uses all those conversions at the toplevel to attempt to rewrite the term. If a conditional rewrite is applied, the resulting theorem will have an assumption. This is the primitive operation that performs HOL Light rewrite steps.

Fails when applied to the term if none of the conversions in the net are applicable.

GENERAL_REWRITE_CONV, GEN_REWRITE_CONV, mk_rewrites, net_of_conv, net_of_thm, REWRITE_CONV.