# Theory Quote_Antiquote

Up to index of Isabelle/HOL/HoareParallel

theory Quote_Antiquote
imports Main
begin

    header {* \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)

    syntax (xsymbols)
      "_Assert"    :: "'a => 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)

    translations
      ".{b}." \<rightharpoonup> "Collect «b»"

    parse_translation {*
      let
        fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
          | quote_tr ts = raise TERM ("quote_tr", ts);
      in [("_quote", quote_tr)] end
    *}

    end