----------------------------------------------------------------------
NOT_CONV                                                   (reduceLib)
----------------------------------------------------------------------
NOT_CONV : conv

SYNOPSIS
Simplifies certain boolean negation expressions.

LIBRARY
reduce

DESCRIBE
If {tm} corresponds to one of the forms given below, where {t} is an arbitrary
term of type {bool}, then {NOT_CONV tm} returns the corresponding theorem.

   NOT_CONV "~F"  = |-  ~F = T
   NOT_CONV "~T"  = |-  ~T = F
   NOT_CONV "~~t" = |- ~~t = t


FAILURE
{NOT_CONV tm} fails unless {tm} has one of the forms indicated above.

EXAMPLE

#NOT_CONV "~~~~T";;
|- ~~~~T = ~~T

#NOT_CONV "~~T";;
|- ~~T = T

#NOT_CONV "~T";;
|- ~T = F


----------------------------------------------------------------------