----------------------------------------------------------------------
list_mk_forall                                            (boolSyntax)
----------------------------------------------------------------------
list_mk_forall : term list * term -> term

SYNOPSIS
Iteratively constructs a universal quantification.

DESCRIBE
{list_mk_forall([x1,...,xn],t)} returns {!x1 ... xn. t}.

FAILURE
Fails if the terms in the list are not variables or if
{t} is not of type {bool} and the list of terms is non-empty. If the list
of terms is empty the type of {t} can be anything.

SEEALSO
boolSyntax.strip_forall, boolSyntax.mk_forall.

----------------------------------------------------------------------