NOT_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Simplifies certain boolean negation expressions.
LIBRARY
reduce
DESCRIPTION
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
HOL  Kananaskis-13