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

UNDISCH : thm -> thm

SYNOPSIS

Undischarges the antecedent of an implicative theorem.

DESCRIPTION

    A |- t1 ==> t2
   ----------------  UNDISCH
     A, t1 |- t2

FAILURE CONDITIONS

UNDISCH will fail on theorems which are not implications.

EXAMPLE

  # UNDISCH(TAUT `p /\ q ==> p`);;
  val it : thm = p /\ q |- p