CONJ_DISCHL
Drule.CONJ_DISCHL : (term list -> thm -> thm)
Conjoins multiple assumptions to both sides of an equation.
Given a term list [t1;...;tn] and a theorem whose conclusion is an
equation between boolean terms, CONJ_DISCHL conjoins all the terms in
the list to both sides of the equation, and removes any of the terms
which were in the assumption list.
A |- s = t
-------------------------------------------------------- CONJ_DISCHL
A - {t1,...,tn} |- (t1/\.../\tn/\s) = (t1/\.../\tn/\t) [t1,...,tn]
Failure
Fails unless the theorem is an equation, both sides of which, and all
the terms provided, are of type bool.