----------------------------------------------------------------------
CONJ_DISCHL                                                    (Drule)
----------------------------------------------------------------------
CONJ_DISCHL : (term list -> thm -> thm)

SYNOPSIS
Conjoins multiple assumptions to both sides of an equation.

KEYWORDS
rule, conjunction, assumption.

DESCRIBE
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}.

SEEALSO
Drule.CONJ_DISCH.

----------------------------------------------------------------------