PART_PMATCH : ((term -> term) -> thm -> term -> thm)
STRUCTURE
PairRules
LIBRARY
pair
SYNOPSIS
Instantiates a theorem by matching part of it to a term.
DESCRIPTION
When applied to a ‘selector’ function of type term -> term, a theorem and a term: 
   PART_MATCH fn (A |- !p1...pn. t) tm
the function PART_PMATCH applies fn to t' (the result of specializing universally quantified pairs in the conclusion of the theorem), and attempts to match the resulting term to the argument term tm. If it succeeds, the appropriately instantiated version of the theorem is returned.
FAILURE
Fails if the selector function fn fails when applied to the instantiated theorem, or if the match fails with the term it has provided.
SEEALSO
PART_MATCH
HOL  Kananaskis-14