MK_DISJ : thm -> thm -> thm

SYNOPSIS

Disjoin both sides of two equational theorems.

DESCRIPTION

Given two theorems, each with a Boolean equation as conclusion, MK_DISJ returns the equation resulting from disjoining their respective sides:

         A |- p <=> p'   B |- q <=> q'
      ----------------------------------- MK_DISJ
           A u B |- p \/ q <=> p' \/ q'

FAILURE CONDITIONS

Fails unless both input theorems are Boolean equations (iff).

EXAMPLE

  # let th1 = ARITH_RULE `1 < x <=> 1 <= x - 1`
    and th2 = ARITH_RULE `~(1 < x) <=> x = 0 \/ x = 1`;;
  val th1 : thm = |- 1 < x <=> 1 <= x - 1
  val th2 : thm = |- ~(1 < x) <=> x = 0 \/ x = 1

  # MK_DISJ th1 th2;;
  val it : thm = |- 1 < x \/ ~(1 < x) <=> 1 <= x - 1 \/ x = 0 \/ x = 1