ONCE_SIMPLIFY_CONV : simpset -> thm list -> conv

SYNOPSIS
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.

SEE ALSO
GEN_SIMPLIFY_CONV, ONCE_DEPTH_SQCONV, SIMPLIFY_CONV, SIMP_CONV, SIMP_RULE, SIMP_TAC.