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

basic_ss : thm list -> simpset

SYNOPSIS: Construct a straightforward simpset from a list of theorems.
DESCRIPTION: In their maximal generality, simplification operations in HOL Light (as invoked by SIMP_TAC) are controlled by a `simpset'. A call basic_ss thl gives a straightforward simpset used by the default simplifier instances like SIMP_TAC, which has the given theorems as well as the basic rewrites and conversions, and no other provers.
FAILURE CONDITIONS: Never fails.
SEE ALSO: basic_convs, basic_rewrites, empty_ss, SIMP_CONV, SIMP_RULE, SIMP_TAC.