----------------------------------------------------------------------
dest_imp                                                  (boolSyntax)
----------------------------------------------------------------------
dest_imp : term -> term * term

SYNOPSIS
Breaks an implication or negation into antecedent and consequent.

DESCRIBE
{dest_imp} is a term destructor for implications. It treats negations as
implications with consequent {F}. Thus, if {M} is a term with the form
{t1 ==> t2}, then {dest_imp M} returns {(t1,t2)}, and if {M} has the
form {~t}, then {dest_imp M} returns {(t,F)}.

FAILURE
Fails if {M} is neither an implication nor a negation.

COMMENTS
Destructs negations for increased functionality of HOL-style resolution.
If the ability to destruct negations is not desired, as is only right,
then use {dest_imp_only}.

SEEALSO
boolSyntax.mk_imp, boolSyntax.dest_imp_only, boolSyntax.is_imp,
boolSyntax.is_imp_only, boolSyntax.strip_imp, boolSyntax.list_mk_imp.

----------------------------------------------------------------------