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
SIMP_RULE : thm list -> thm -> thm
SYNOPSIS
Simplify conclusion of a theorem repeatedly by conditional contextual
rewriting.
DESCRIPTION
A call SIMP_CONV thl (|- tm) will return |- tm' where tm' results from
applying the theorems in thl as (conditional) rewrite rules, as well as
built-in simplifications (see basic_rewrites and basic_convs). For more
details on this kind of conditional rewriting, see SIMP_CONV.
FAILURE CONDITIONS
Never fails, but may return the input theorem unchanged if no simplifications
were applicable.