PGEN_TAC : tactic
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Strips the outermost paired universal quantifier from the conclusion of a goal.
DESCRIPTION
When applied to a goal A ?- !p. t, the tactic PGEN_TAC reduces it to A ?- t[p'/p] where p' is a variant of the paired variable structure p chosen to avoid clashing with any variables free in the goal’s assumption list. Normally p' is just p. 
     A ?- !p. t
   ==============  PGEN_TAC
    A ?- t[p'/p]

FAILURE
Fails unless the goal’s conclusion is a paired universally quantification.
SEEALSO
GEN_TAC, FILTER_PGEN_TAC, PGEN, PGENL, PSPEC, PSPECL, PSPEC_ALL, PSPEC_TAC, PSTRIP_TAC, P_PGEN_TAC
HOL  Kananaskis-14