1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
\DOC SIMPLIFY_CONV
\TYPE {SIMPLIFY_CONV : simpset -> thm list -> conv}
\SYNOPSIS
General simplification at depth with arbitrary simpset.
\DESCRIBE
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
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.
\SEEALSO
GEN_SIMPLIFY_CONV, ONCE_SIMPLIFY_CONV, SIMP_CONV, SIMP_RULE, SIMP_TAC,
TOP_DEPTH_SQCONV.
\ENDDOC
|
