Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
ss_of_congs : thm list -> simpset -> simpset
SYNOPSIS
Add congruence rules to a simpset.
DESCRIPTION
In their maximal generality, simplification operations in HOL Light (as invoked
by SIMP_TAC) are controlled by a `simpset', which may contain conditional and
unconditional rewrite rules, conversions and provers for conditions, as well as
a determination of how to use the prover on the conditions and how to process
theorems into rewrites. A call ss_of_congs thl ss adds thl as new
congruence rules to the simpset ss to yield a new simpset. For an
illustration of how congruence rules can be used, see extend_basic_congs.
FAILURE CONDITIONS
Never fails unless the congruence rules are malformed.