\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
}
\noindent {ADD_ASSUM} performs straightforward set union with the new
assumption; it checks for identical assumptions, but not for alpha-equivalent
ones. The position at which the new assumption is inserted into the assumption
list should not be relied on.

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

\SEEALSO
ASSUME, UNDISCH.

\ENDDOC