----------------------------------------------------------------------
PART_MATCH_A                                                   (Drule)
----------------------------------------------------------------------
PART_MATCH_A : (term -> term) -> thm -> term -> thm

SYNOPSIS
Instantiates a theorem by matching part of its conclusion to a term.

DESCRIBE
{PART_MATCH_A} behaves as {PART_MATCH} except that it permits instantiating
variables which appear in the assumptions of the given theorem.

SEEALSO
Drule.PART_MATCH, Conv.REWR_CONV_A.

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