dest_neg : term -> term
STRUCTURE
boolSyntax
SYNOPSIS
Breaks apart a negation, returning its body.
DESCRIPTION
dest_neg
is a term destructor for negations: if
M
has the form
~t
, then
dest_neg M
returns
t
.
FAILURE
Fails with
dest_neg
if term is not a negation.
SEEALSO
mk_neg
,
is_neg
HOL
Kananaskis-13