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.