PGENL : (term list -> thm -> thm)

- STRUCTURE
- 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

HOL Kananaskis-14