PBETA_TAC : tactic
STRUCTURE
LIBRARY
pair
SYNOPSIS
Beta-reduces all the paired beta-redexes in the conclusion of a goal.
DESCRIPTION
When applied to a goal A ?- t, the tactic PBETA_TAC produces a new goal which results from beta-reducing all paired beta-redexes, at any depth, in t. Variables are renamed where necessary to avoid free variable capture.
    A ?- ...((\p. s1) s2)...
   ==========================  PBETA_TAC
     A ?- ...(s1[s2/p])...

FAILURE
Never fails, but will have no effect if there are no paired beta-redexes.
SEEALSO
HOL  Kananaskis-13