BasicProvers.Abbr

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.