UNDISCH_ALL : thm -> thm

SYNOPSIS

Iteratively undischarges antecedents in a chain of implications.

DESCRIPTION

    A |- t1 ==> ... ==> tn ==> t
   ------------------------------  UNDISCH_ALL
        A, t1, ..., tn |- t

FAILURE CONDITIONS

Unlike UNDISCH, UNDISCH_ALL will, when called on something other than an implication, return its argument unchanged rather than failing.

EXAMPLE

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