Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
ONCE_DEPTH_SQCONV : strategy
SYNOPSIS
Applies simplification to the first suitable sub-term(s) encountered in
top-down order.
DESCRIPTION
HOL Light's simplification functions (e.g. SIMP_TAC) have their traversal
algorithm controlled by a ``strategy''. ONCE_DEPTH_SQCONV is a strategy
corresponding to ONCE_DEPTH_CONV for ordinary conversions: simplification is
applied to the first suitable subterm(s) encountered in top-down order.