mk_forall : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Term constructor for universal quantification.
DESCRIPTION
If
v
is a variable and
t
is a term of type
bool
, then
mk_forall (v,t)
returns the term
!v. t
.
FAILURE
Fails if
v
is not a variable or if
t
is not of type
bool
.
SEEALSO
dest_forall
,
is_forall
,
list_mk_forall
,
strip_forall
HOL
Trindemossen-1