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