CONJ_DISCH : (term -> thm -> thm)
STRUCTURE
SYNOPSIS
Discharges an assumption and conjoins it to both sides of an equation.
DESCRIPTION
Given an term t and a theorem A |- t1 = t2, which is an equation between boolean terms, CONJ_DISCH returns A - {t} |- (t /\ t1) = (t /\ t2), i.e. conjoins t to both sides of the equation, removing t from the assumptions if it was there.
            A |- t1 = t2
   ------------------------------  CONJ_DISCH "t"
    A - {t} |- t /\ t1 = t /\ t2

FAILURE
Fails unless the theorem is an equation, both sides of which, and the term provided are of type bool.
SEEALSO
HOL  Trindemossen-1