----------------------------------------------------------------------
BETA_CONV                                                        (Thm)
----------------------------------------------------------------------
BETA_CONV : conv

SYNOPSIS
Performs a single step of beta-conversion.

KEYWORDS
conversion.

DESCRIBE
The conversion {BETA_CONV} maps a beta-redex {"(\x.u)v"} to the theorem

   |- (\x.u)v = u[v/x]

where {u[v/x]} denotes the result of substituting {v} for all free
occurrences of {x} in {u}, after renaming sufficient bound variables to avoid
variable capture. This conversion is one of the primitive inference rules of
the HOL system.

FAILURE
{BETA_CONV tm} fails if {tm} is not a beta-redex.

EXAMPLE

- BETA_CONV (Term `(\x.x+1)y`);
> val it = |- (\x. x + 1)y = y + 1 :thm

- BETA_CONV (Term `(\x y. x+y)y`);
> val it = |- (\x y. x + y)y = (\y'. y + y') : thm




SEEALSO
Conv.BETA_RULE, Tactic.BETA_TAC, Drule.LIST_BETA_CONV,
PairedLambda.PAIRED_BETA_CONV, Drule.RIGHT_BETA,
Drule.RIGHT_LIST_BETA.

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