Q.HO_MATCH_ABBREV_TAC : term quotation -> tactic
STRUCTURE
SYNOPSIS
Introduces abbreviations by doing a higher-order match against the goal.
DESCRIPTION
This tactic is just like Q.MATCH_ABBREV_TAC, but does a higher-order match against the goal rather than a first order match. See the documentation for MATCH_ABBREV_TAC for more details.
EXAMPLE
The goal
   ?- !n. (n + 1) * (n - 1) = n * n - 1
is transformed by Q.HO_MATCH_ABBREV_TAC `!k. P k` to
   Abbrev(P = (\n. (n + 1) * (n - 1) = n * n - 1)) ?-  !k. P k
Note how the bound variable changes to match that used in the pattern.
SEEALSO
HOL  Kananaskis-13