REDEPTH_CONSEQ_CONV

ConseqConv.REDEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv

Similar to DEPTH_CONSEQ_CONV, but revisits modified subterms.

See also

ConseqConv.DEPTH_CONSEQ_CONV