dest_pabs : term -> term * term
STRUCTURE
pairSyntax
LIBRARY
pair
SYNOPSIS
Breaks apart a paired abstraction into abstracted pair and body.
DESCRIPTION
dest_pabs
is a term destructor for paired abstractions:
dest_abs "\pair. t"
returns
("pair","t")
.
FAILURE
Fails with
dest_pabs
if term is not a paired abstraction.
SEEALSO
dest_abs
,
mk_pabs
,
is_pabs
,
strip_pabs
HOL
Kananaskis-13