dest_pselect : term -> term * term
STRUCTURE
LIBRARY
pair
SYNOPSIS
Breaks apart a paired choice-term into the selected pair and the body.
DESCRIPTION
dest_pselect is a term destructor for paired choice terms. The application of dest_select to @pair. t returns (pair,t).
FAILURE
Fails with dest_pselect if term is not a paired choice-term.
SEEALSO
HOL  Kananaskis-13