mk_neg : (term -> term)
STRUCTURE
boolSyntax
SYNOPSIS
Constructs a negation.
DESCRIPTION
mk_neg "t"
returns
"~t"
.
FAILURE
Fails with
mk_neg
unless
t
is of type
bool
.
SEEALSO
dest_neg
,
is_neg
HOL
Kananaskis-14