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.