list_mk_abs : term list * term -> term
STRUCTURE
Term
SYNOPSIS
Performs a sequence of lambda binding operations.
DESCRIPTION
An application list_mk_abs ([v1,...,vn], M) yields the term \v1 ... vn. M. Free occurrences of v1,...,vn in M become bound in the result.
FAILURE
Fails if some vi (1 <= i <= n) is not a variable.
EXAMPLE
- list_mk_abs ([mk_var("v1",bool),mk_var("v2",bool),mk_var("v3",bool)],
               Term `v1 /\ v2 /\ v3`);
> val it = `\v1 v2 v3. v1 /\ v2 /\ v3` : term

COMMENTS
In the current implementation, list_mk_abs is more efficient than iteration of mk_abs for larger tasks.
SEEALSO
mk_abs, list_mk_forall, list_mk_exists
HOL  Kananaskis-13