ONCE_SIMPLIFY_CONV : simpset -> thm list -> conv
General top-level simplification with arbitrary simpset.
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
- FAILURE CONDITIONS
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,