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

SEE ALSO