\DOC ADD_ASSUM

\TYPE {ADD_ASSUM : term -> thm -> thm}

\SYNOPSIS
Adds an assumption to a theorem.

\KEYWORDS
rule, assumption.

\DESCRIBE
When applied to a boolean term {s} and a theorem {A |- t}, the
inference rule {ADD_ASSUM} returns the theorem {A u {s} |- t}.
{
       A |- t
   --------------  ADD_ASSUM s
    A u {s} |- t
}

\FAILURE
Fails unless the given term has type {bool}.

\SEEALSO
Thm.ASSUME, Drule.UNDISCH.
\ENDDOC