strip_forall : term -> term list * term
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart universal quantifications.
DESCRIPTION
If
M
has the form
!x1 ... xn. t
then
strip_forall M
returns
([x1,...,xn],t)
. Note that
strip_forall(list_mk_forall([x1,...,xn],t,))
will not return
([x1,...,xn],t)
if
t
is a universal quantification.
FAILURE
Never fails.
SEEALSO
list_mk_forall
,
dest_forall
HOL
Kananaskis-10