1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
\DOC REDEPTH_SQCONV
\TYPE {REDEPTH_SQCONV : strategy}
\SYNOPSIS
Applies simplification bottom-up to all subterms, retraversing changed ones.
\DESCRIBE
HOL Light's simplification functions (e.g. {SIMP_TAC}) have their traversal
algorithm controlled by a ``strategy''. {REDEPTH_SQCONV} is a strategy
corresponding to {REDEPTH_CONV} for ordinary conversions: simplification is
applied bottom-up to all subterms, retraversing changed ones.
\FAILURE
Not applicable.
\SEEALSO
DEPTH_SQCONV, ONCE_DEPTH_SQCONV, REDEPTH_CONV, TOP_DEPTH_SQCONV,
TOP_SWEEP_SQCONV.
\ENDDOC
|
