Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456

DISJ2 : term -> thm -> thm

SYNOPSIS

Introduces a left disjunct into the conclusion of a theorem.

DESCRIPTION

      A |- t2
   ---------------  DISJ2 `t1`
    A |- t1 \/ t2

FAILURE CONDITIONS

Fails if the term argument is not boolean.

EXAMPLE

  # DISJ2 `F` TRUTH;;
  val it : thm = |- F \/ T