Theory Sharp_Syntax

theory Sharp_Syntax
imports Main Adhoc_Overloading
(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2015)
License: LGPL (see file COPYING.LESSER)
*)

section ‹Overloading for the Sharp Symbol›

theory Sharp_Syntax
imports
  Main
  "~~/src/Tools/Adhoc_Overloading"
begin

consts SHARP :: "'a ⇒ 'b" ("♯")

locale sharp_syntax =
  fixes shp :: "'f ⇒ 'f"
begin

adhoc_overloading SHARP shp

end

end