REWRITES_CONV : ('a * (term -> 'b)) net -> term -> 'b
SYNOPSIS
Apply a prioritized conversion net to the term at the top level.
DESCRIPTION
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.
FAILURE CONDITIONS
Fails when applied to the term if none of the conversions in the net are
applicable.