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``]);
val it = [``A = T``,``B = 3``] : term list

SEEALSO
filter
HOL  Trindemossen-1