TOP_DEPTH_SQCONV : strategy
Applies simplification top-down to all subterms, retraversing changed ones.
HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal
algorithm controlled by a ``strategy''. TOP_DEPTH_SQCONV is a strategy
corresponding to TOP_DEPTH_CONV for ordinary conversions: simplification is
applied top-down to all subterms, retraversing changed ones.
- FAILURE CONDITIONS
- SEE ALSO
DEPTH_SQCONV, ONCE_DEPTH_SQCONV, REDEPTH_SQCONV, TOP_DEPTH_CONV,