PART_MATCH_A : (term -> term) -> thm -> term -> thm
STRUCTURE
Drule
SYNOPSIS
Instantiates a theorem by matching part of its conclusion to a term.
DESCRIPTION
PART_MATCH_A
behaves as
PART_MATCH
except that it permits instantiating variables which appear in the assumptions of the given theorem.
SEEALSO
PART_MATCH
,
REWR_CONV_A
HOL
Kananaskis-14