Abbr
BasicProvers.Abbr : term quotation -> thm
Signals to simplification tactics that an abbreviation should be used.
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.