ONCE_DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
STRUCTURE
SYNOPSIS
Applies a consequence conversion at most once to a sub-terms of a term.
DESCRIPTION
While DEPTH_CONSEQ_CONV c tm applies c repeatedly, ONCE_DEPTH_CONSEQ_CONV c tm applies c at most once.
SEEALSO
HOL  Trindemossen-1