----------------------------------------------------------------------
Abbr                                                    (BasicProvers)
----------------------------------------------------------------------
BasicProvers.Abbr : term quotation -> thm

SYNOPSIS
Signals to simplification tactics that an abbreviation should be used.

DESCRIBE
The {Abbr} function is used to signal to various simplification
tactics that an abbreviation in the current goal should be eliminated
before simplification proceeds.  Each theorem created by {Abbr} is
removed from the tactic’s theorem-list argument, and causes a call to
{Q.UNABBREV_TAC} with that {Abbr} theorem’s argument.  Finally, the
simplification tactic continues, with the rest of the theorem-list as
its argument.  Thus,

   tac [..., Abbr`v`, ..., Abbr`u`, ...]

has the same effect as

   Q.UNABBREV_TAC `v` THEN Q.UNABBREV_TAC `u` THEN
   tac [..., ..., ...]

Every theorem created by {Abbr} in the argument list is treated in
this way.  The tactics that understand {Abbr} arguments are
{SIMP_TAC}, {ASM_SIMP_TAC}, {FULL_SIMP_TAC}, {RW_TAC} and {SRW_TAC}.

FAILURE
{Abbr} itself never fails, but the tactic it is used in may do,
particularly if the induced calls to {UNABBREV_TAC} fail.

COMMENTS
This function is a notational convenience that allows the effect of
multiple tactics to be packaged into just one.

SEEALSO
Q.ABBREV_TAC, simpLib.SIMP_TAC, Q.UNABBREV_TAC.

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