is_imp : term -> bool
STRUCTURE
SYNOPSIS
Tests a term to see if it is an implication or a negation.
DESCRIPTION
If M has the form t1 ==> t2, or the form ~t, then is_imp M returns true. If the term is neither an implication nor a negation the result is false.
FAILURE
Never fails.
COMMENTS
Yields true of negations because dest_imp destructs negations (for backwards compatibility with PPLAMBDA). Use is_imp_only if you don’t want this behaviour.
SEEALSO
HOL  Kananaskis-13