mk_exists1 : term * term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Term constructor for unique existence.
DESCRIPTION
If
v
is a variable and
t
is a term of type
bool
, then
mk_exists1 (v,t)
returns the term
?!v. t
.
FAILURE
Fails if
v
is not a variable or if
t
is not of type
bool
.
SEEALSO
dest_exists1
,
is_exists1
HOL
Kananaskis-13