GEN_SIMPLIFY_CONV : strategy -> simpset -> int -> thm list -> conv

SYNOPSIS: General simplification with given strategy and simpset and theorems.
DESCRIPTION: The call GEN_SIMPLIFY_CONV strat ss n thl incorporates the rewrites and conditional rewrites derived from thl into the simpset ss, then simplifies using that simpset, controlling the traversal of the term by strat, and starting at level n.
FAILURE CONDITIONS: Never fails unless some component is malformed.
SEE ALSO: GEN_REWRITE_CONV, ONCE_SIMPLIFY_CONV, SIMPLIFY_CONV, SIMP_CONV, SIMP_RULE, SIMP_TAC.