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.
- SEE ALSO
- mk_rewrites, net_of_cong, net_of_conv, REWRITES_CONV.