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
28
|
\DOC ONCE_SIMPLIFY_CONV
\TYPE {ONCE_SIMPLIFY_CONV : simpset -> thm list -> conv}
\SYNOPSIS
General top-level simplification 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
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
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_DEPTH_SQCONV, SIMPLIFY_CONV, SIMP_CONV, SIMP_RULE,
SIMP_TAC.
\ENDDOC
|
