NOT_CONV : conv

- STRUCTURE
- 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-14