SIMPLIFY_CONV : simpset -> thm list -> conv

- SYNOPSIS
- General simplification at depth 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 repeated top-down traversal strategy (TOP_DEPTH_SQCONV) and a nesting limit of 3 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_SIMPLIFY_CONV, SIMP_CONV, SIMP_RULE, SIMP_TAC, TOP_DEPTH_SQCONV.