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