HYP_CONV_RULE : (term -> bool) -> (conv -> thm -> thm)
STRUCTURE
SYNOPSIS
Makes an inference rule by applying a conversion to hypotheses of a theorem.
DESCRIPTION
If conv is a conversion, then HYP_CONV_RULE sel conv is an inference rule that applies conv to those hypotheses of a theorem which are selected by sel. That is, if conv maps a term "h" to the theorem |- h = h', then the rule HYP_CONV_RULE sel conv infers A, h' |- c from the theorem A, h |- c. More precisely, if conv "h" returns A' |- h = h', then:
       A, h |- c
   ----------------  HYP_CONV_RULE sel conv
    A u A', h' |- c
Note that if the conversion conv returns a theorem with assumptions, then the resulting inference rule adds these to the assumptions of the theorem it returns.
FAILURE
HYP_CONV_RULE sel conv th fails if sel fails when applied to a hypothesis of th, or if conv fails when applied to a hypothesis selected by sel. The function returned by HYP_CONV_RULE sel conv will also fail if the ML function conv:term->thm is not, in fact, a conversion (i.e. a function that maps a term h to a theorem |- h = h').
SEEALSO
HOL  Kananaskis-13