dest_imp_only
boolSyntax.dest_imp_only : term -> term * term
Breaks an implication into antecedent and consequent.
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.
See also
boolSyntax.mk_imp,
boolSyntax.dest_imp,
boolSyntax.is_imp,
boolSyntax.is_imp_only,
boolSyntax.strip_imp,
boolSyntax.list_mk_imp