type directed_conseq_conv
STRUCTURE
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
HOL  Trindemossen-1