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_TAC : thm list -> tactic

SYNOPSIS: Simplify a goal repeatedly by conditional contextual rewriting.
DESCRIPTION: When applied to a goal A ?- g, the tactic SIMP_TAC thl returns a new goal A ?- g' where g' 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, see SIMP_CONV.
FAILURE CONDITIONS: Never fails, though may not change the goal if no simplifications are applicable.
COMMENTS: To add the assumptions of the goal to the rewrites, use ASM_SIMP_TAC (or just ASM SIMP_TAC).
SEE ALSO: ASM, ASM_SIMP_TAC, IMP_REWRITE_TAC, mk_rewrites, ONCE_SIMP_CONV, REWRITE_TAC, SIMP_CONV, SIMP_RULE, TARGET_REWRITE_TAC.