is_imp_only : term -> bool
STRUCTURE
boolSyntax
SYNOPSIS
Tests a term to see if it is an implication.
DESCRIPTION
If
M
has the form
t1 ==> t2
then
is_imp_only M
returns
true
. If the term is not an implication, the result is
false
.
FAILURE
Never fails.
SEEALSO
is_imp
,
mk_imp
,
dest_imp
,
dest_imp_only
,
list_mk_imp
,
strip_imp
HOL
Kananaskis-13