mk_forall
boolSyntax.mk_forall : term * term -> term
Term constructor for universal quantification.
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.
See also
boolSyntax.dest_forall,
boolSyntax.is_forall,
boolSyntax.list_mk_forall,
boolSyntax.strip_forall