is_forall : term -> bool
STRUCTURE
boolSyntax
SYNOPSIS
Tests a term to see if it is a universal quantification.
DESCRIPTION
If
M
is a term with the form
!x. t
, then
is_forall M
returns
true
. If
M
is not a universal quantification the result is
false
.
FAILURE
Never fails.
SEEALSO
mk_forall
,
dest_forall
HOL
Kananaskis-14