Theory HOL-Hoare_Parallel.Quote_Antiquote

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 \<^syntax_const>‹_antiquote› t
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(\<^syntax_const>‹_quote›, K quote_tr)] end
›

end