Provide "backup copies" of the old implementations of the abbreviation
tactics so that old proofs (such as those in the arm6 examples) can go
through even as the abbreviation tactics evolve. First evolution is to
modify UNABBREV_TAC to remove the abbreviation assumption, and to do
a SUBST_ALL_TAC rather than just a SUBST1_TAC.