General top-level simplification with arbitrary simpset.
DESCRIPTION
In their maximal generality, simplification operations in HOL Light (as invoked
by SIMP_TAC) are controlled by a `simpset'. Given a simpset ss and an
additional list of theorems thl to be used as (conditional or unconditional)
rewrite rules, SIMPLIFY_CONV ss thl gives a simplification conversion with a
top-down single simplification traversal strategy (ONCE_DEPTH_SQCONV) and a
nesting limit of 1 for the recursive solution of subconditions by further
simplification.
FAILURE CONDITIONS
Never fails.
USES
Usually some other interface to the simplifier is more convenient, but you may
want to use this to employ a customized simpset.