Applies simplification top-down at all levels, but after descending to
subterms, does not return to higher ones.
DESCRIPTION
HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal
algorithm controlled by a ``strategy''. TOP_SWEEP_SQCONV is a strategy
corresponding to TOP_SWEEP_CONV for ordinary conversions: simplification is
applied top-down at all levels, but after descending to subterms, does not
return to higher ones.