REDEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
STRUCTURE
SYNOPSIS
Similar to DEPTH_CONSEQ_CONV, but revisits modified subterms.
SEEALSO
HOL  Trindemossen-1