dest_imp_only : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks an implication into antecedent and consequent.
DESCRIPTION
If M is a term with the form t1 ==> t2, then dest_imp_only M returns (t1,t2).
FAILURE
Fails if M is not an implication.
SEEALSO
mk_imp, dest_imp, is_imp, is_imp_only, strip_imp, list_mk_imp
HOL  Kananaskis-14