dest_forall : term -> term * term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart a universally quantified term into quantified variable and body.
DESCRIPTION
If
M
has the form
!x. t
, then
dest_forall M
returns
(x,t)
.
FAILURE
Fails if
M
is not a universal quantification.
SEEALSO
mk_forall
,
is_forall
,
strip_forall
,
list_mk_forall
HOL
Kananaskis-13