MK_DISJ : thm -> thm -> thm
A |- p <=> p' B |- q <=> q' ----------------------------------- MK_DISJ A u B |- p \/ q <=> p' \/ q'
# 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