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