PGENL : (term list -> thm -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Generalizes zero or more pairs in the conclusion of a theorem.
DESCRIPTION
When applied to a list of paired variable structures [p1;...;pn] and a theorem A |- t, the inference rule PGENL returns the theorem A |- !p1...pn. t, provided none of the constituent variables from any of the pairs pi occur free in the assumptions. 
         A |- t
   ------------------  PGENL "[p1;...;pn]"       [where no pi is free in A]
    A |- !p1...pn. t

FAILURE
Fails unless all the terms in the list are paired structures of variables, none of the variables from which are free in the assumption list.
SEEALSO
GENL, PGEN, PGEN_TAC, PSPEC, PSPECL, PSPEC_ALL, PSPEC_TAC
HOL  Kananaskis-13