GEN_PALPHA_CONV : term -> conv

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Renames the bound pair of a paired abstraction, quantified term, or other binder.
- DESCRIPTION
- The conversion GEN_PALPHA_CONV provides alpha conversion for lambda abstractions of the form \p.t, quantified terms of the forms !p.t, ?p.t or ?!p.t, and epsilon terms of the form @p.t.
The renaming of pairs is as described for PALPHA_CONV.

- FAILURE
- GEN_PALPHA_CONV q tm fails if q is not a variable, or if tm does not have one of the required forms. GEN_ALPHA_CONV q tm also fails if tm does have one of these forms, but types of the variables p and q differ.
- SEEALSO

HOL Kananaskis-14