UNPBETA_CONV : (term -> conv)
STRUCTURE
LIBRARY
pair
SYNOPSIS
Creates an application of a paired abstraction from a term.
DESCRIPTION
The user nominates some pair structure of variables p and a term t, and UNPBETA_CONV turns t into an abstraction on p applied to p.
   ------------------  UNPBETA_CONV "p" "t"
    |- t = (\p. t) p

FAILURE
Fails if p is not a paired structure of variables.
SEEALSO
HOL  Kananaskis-10