Theory Sharp_Syntax

(*
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
  "HOL-Library.Adhoc_Overloading"
begin

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

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

adhoc_overloading SHARP shp

end

end