Quelle  Quote_Antiquote.thy   Sprache: Isabelle

section ‹Concrete Syntax›

theory Quote_Antiquote imports Main begin

syntax
  "_quote"     :: "'b \ ('a \ 'b)"                (‹(«_¬)› [0] 1000)
  "_antiquote" :: "('a \ 'b) \ 'b"                (‹🍋_› [1000] 1000)
  "_Assert"    :: "'a \ 'a set"                    (‹({_})› [0] 1000)

translations
  "\b\" ⇀ "CONST Collect \b\"

parse_translation ‹
  let
    fun quote_tr [t] = Syntax_Trans.quote_tr 🍋‹_antiquote› t
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(🍋‹_quote›, K quote_tr)] end
›

end