net_of_cong : thm -> (int * (term -> thm)) net -> (int * (term -> thm)) net
- SYNOPSIS
-
Add a congruence rule to a net.
- 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. The congruence rules used by the simplifier to establish
context (see extend_basic_congs) are also stored in this structure, with the
lowest priority 4. A call net_of_cong th net adds th as a new congruence
rule to net to yield an updated net.
- FAILURE CONDITIONS
-
Fails unless the congruence is of the appropriate implicational form.
- SEE ALSO
-
extend_basic_congs, net_of_conv, net_of_thm.