1\DOC BETA_TAC
2
3\TYPE {BETA_TAC : tactic}
4
5\SYNOPSIS
6Beta-reduces all the beta-redexes in the conclusion of a goal.
7
8\KEYWORDS
9tactic.
10
11\DESCRIBE
12When applied to a goal {A ?- t}, the tactic {BETA_TAC} produces a new goal
13which results from beta-reducing all beta-redexes, at any depth, in {t}.
14Variables are renamed where necessary to avoid free variable capture.
15{
16    A ?- ...((\x. s1) s2)...
17   ==========================  BETA_TAC
18     A ?- ...(s1[s2/x])...
19}
20
21
22\FAILURE
23Never fails, but will have no effect if there are no beta-redexes.
24
25\SEEALSO
26Thm.BETA_CONV, Tactic.BETA_TAC, PairedLambda.PAIRED_BETA_CONV.
27\ENDDOC
28