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.