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.