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