OR_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Simplifies certain boolean disjunction expressions.
LIBRARY
reduce
DESCRIPTION
If tm corresponds to one of the forms given below, where t is an arbitrary term of type bool, then OR_CONV tm returns the corresponding theorem. Note that in the last case the disjuncts need only be alpha-equivalent rather than strictly identical. 
   OR_CONV "T \/ t" = |- T \/ t = T
   OR_CONV "t \/ T" = |- t \/ T = T
   OR_CONV "F \/ t" = |- F \/ t = t
   OR_CONV "t \/ F" = |- t \/ F = t
   OR_CONV "t \/ t" = |- t \/ t = t
FAILURE
OR_CONV tm fails unless tm has one of the forms indicated above.
EXAMPLE
#OR_CONV "F \/ T";;
|- F \/ T = T

#OR_CONV "X \/ F";;
|- X \/ F = X

#OR_CONV "(!n. n + 1 = SUC n) \/ (!m. m + 1 = SUC m)";;
|- (!n. n + 1 = SUC n) \/ (!m. m + 1 = SUC m) = (!n. n + 1 = SUC n)
HOL  Kananaskis-13