Source File | Identifier index | Theory binding index |
---|
signature OldAbbrevTactics = sig include Abbrev val ABBREV_TAC : term quotation -> tactic val UNABBREV_TAC : term quotation -> tactic val PAT_ABBREV_TAC : term quotation -> tactic end
Source File | Identifier index | Theory binding index |
---|