type CONSEQ_CONV_direction
STRUCTURE
SYNOPSIS
A type used to tell directed consequence conversions what the desired result should look like.
DESCRIPTION
This type is used to instruct a directed consequence conversion how to behave. Given a direction dir and a boolean term t the result of a directed consequence conversion DCONSEQ_CONV should be of the form
- st ==> t for dir = CONSEQ_CONV_STRENGTHEN_direction
- t ==> wt for dir = CONSEQ_CONV_WEAKEN_direction
- st ==> t, t ==> wt or t = eqt for dir = CONSEQ_CONV_UNKNOWN_direction
SEEALSO
HOL  Kananaskis-14