ONCE_DEPTH_CONSEQ_CONV : directed_conseq_conv -> directed_conseq_conv
STRUCTURE
ConseqConv
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
DEPTH_CONV
,
NUM_DEPTH_CONSEQ_CONV
,
DEPTH_CONSEQ_CONV
,
DEPTH_STRENGTHEN_CONSEQ_CONV
HOL
Kananaskis-14