BETA_RULE : (thm -> thm)
STRUCTURE
Conv
SYNOPSIS
Beta-reduces all the beta-redexes in the conclusion of a theorem.
DESCRIPTION
When applied to a theorem A |- t, the inference rule BETA_RULE beta-reduces all beta-redexes, at any depth, in the conclusion t. Variables are renamed where necessary to avoid free variable capture. 
    A |- ....((\x. s1) s2)....
   ----------------------------  BETA_RULE
      A |- ....(s1[s2/x])....

FAILURE
Never fails, but will have no effect if there are no beta-redexes.
EXAMPLE
The following example is a simple reduction which illustrates variable renaming: 
   - Globals.show_assums := true;
   val it = () : unit

   - local val tm = Parse.Term `f = ((\x y. x + y) y)`
     in
     val x = ASSUME tm
     end;
   val x = [f = (\x y. x + y)y] |- f = (\x y. x + y)y : thm

   - BETA_RULE x;
   val it = [f = (\x y. x + y)y] |- f = (\y'. y + y') : thm

SEEALSO
BETA_CONV, BETA_TAC, PAIRED_BETA_CONV, RIGHT_BETA
HOL  Kananaskis-13