net_of_thm : bool -> thm -> (int * (term -> thm)) net -> (int * (term -> thm)) net
SYNOPSIS
Insert a theorem into a net as a (conditional) rewrite.
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. Such a net can then be used by REWRITES_CONV. A call
net_of_thm rf th net where th is a pure or conditional equation (as
constructed by mk_rewrites, for example) will insert that rewrite rule into
the net with priority 1 (the highest) for a pure rewrite or 3 for a
conditional rewrite, to yield an updated net.
If rf is true, it indicates that this net will be used for repeated
rewriting (e.g. as in REWRITE_CONV rather than ONCE_REWRITE_CONV), and
therefore equations are simply discarded without changing the net if the LHS
occurs free in the RHS. This does not exclude more complicated looping
situations, but is still useful.
FAILURE CONDITIONS
Fails on a theorem that is neither a pure nor conditional equation.