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