Structure OldAbbrevTactics


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

HOL 4, Trindemossen-1