type directed_conseq_conv
STRUCTURE
ConseqConv
SYNOPSIS
A type for consequence conversions that can be instructed on whether to strengthen or weaken a given term.
DESCRIPTION
Given a
CONSEQ_CONV_direction
, a directed consequence conversion tries to strengthen, weaken or whatever it can depending on the given direction.
SEEALSO
conseq_conv
,
CONSEQ_CONV_direction
HOL
Kananaskis-13