NUM_DEPTH_CONSEQ_CONV : directed_conseq_conv -> int -> directed_conseq_conv
STRUCTURE
SYNOPSIS
Applies a consequence conversion at most a given number of times to the sub-terms of a term, in bottom-up order.
DESCRIPTION
While DEPTH_CONSEQ_CONV c tm applies c repeatedly, NUM_DEPTH_CONSEQ_CONV c n tm applies it at most n-times.
SEEALSO
HOL  Trindemossen-1