body : term -> term
STRUCTURE
Term
SYNOPSIS
Returns the body of an abstraction.
DESCRIPTION
If
M
is a lambda abstraction, i.e, has the form
\v. t
, then
body M
returns
t
.
FAILURE
Fails unless
M
is an abstraction.
SEEALSO
bvar
,
dest_abs
HOL
Kananaskis-14