ADD_ASSUM : term -> thm -> thm
STRUCTURE
Drule
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
FAILURE
Fails unless the given term has type bool.
SEEALSO
ASSUME, UNDISCH
HOL  Kananaskis-10