disch : ((term * term list) -> term list)
STRUCTURE
HolKernel
SYNOPSIS
Removes those elements of a list of terms that are alpha equivalent to a given term.
DESCRIPTION
Given a pair (t,tl) of term t and term list tl, disch removes those elements of tl that are alpha equivalent to t.
EXAMPLE
disch (``\x:bool.T``, [``A = T``, ``B = 3``, ``\y:bool.T``]);
[`A = T`,`B = 3`] : term list

SEEALSO
filter
HOL  Kananaskis-8