ONCE_DEPTH_CONSEQ_CONV
ConseqConv.ONCE_DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
Applies a consequence conversion at most once to a sub-terms of a term.
While DEPTH_CONSEQ_CONV c tm applies c repeatedly,
ONCE_DEPTH_CONSEQ_CONV c tm applies c at most once.
See also
Conv.DEPTH_CONV,
ConseqConv.NUM_DEPTH_CONSEQ_CONV,
ConseqConv.DEPTH_CONSEQ_CONV,
ConseqConv.DEPTH_STRENGTHEN_CONSEQ_CONV