ADD_ASSUM : term -> thm -> thm

SYNOPSIS

Adds an assumption to a theorem.

DESCRIPTION

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

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 CONDITIONS

Fails unless the given term has type bool.

EXAMPLE

  # ADD_ASSUM `q:bool` (ASSUME `p:bool`);;
  val it : thm = p, q |- p

SEE ALSO

ASSUME, UNDISCH.