mk_res_forall : (term # term # term) -> term
STRUCTURE
res_quanLib
SYNOPSIS
Term constructor for restricted universal quantification.
DESCRIPTION
mk_res_forall("var","P","t")
returns
"!var :: P . t"
.
FAILURE
Fails with
mk_res_forall
if the first term is not a variable or if
P
and
t
are not of type
":bool"
.
SEEALSO
dest_res_forall
,
is_res_forall
,
list_mk_res_forall
HOL
Kananaskis-14