mk_abs : term * term -> term
STRUCTURE
SYNOPSIS
Constructs an abstraction.
DESCRIPTION
mk_abs (v, t) returns the lambda abstraction \v. t. All free occurrences of v in t thereby become bound.
FAILURE
Fails if v is not a variable.
SEEALSO
HOL  Kananaskis-13