1signature OldAbbrevTactics = 2sig 3 include Abbrev 4 5 val ABBREV_TAC : term quotation -> tactic 6 val UNABBREV_TAC : term quotation -> tactic 7 val PAT_ABBREV_TAC : term quotation -> tactic 8 9end 10