----------------------------------------------------------------------
HO_MATCH_ABBREV_TAC                                                (Q)
----------------------------------------------------------------------
Q.HO_MATCH_ABBREV_TAC : term quotation -> tactic

SYNOPSIS
Introduces abbreviations by doing a higher-order match against the goal.

DESCRIBE
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
Q.ABBREV_TAC, Q.MATCH_ABBREV_TAC.

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