src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author wenzelm
Thu May 24 17:25:53 2012 +0200 (2012-05-24)
changeset 47988 e4b69e10b990
parent 42284 326f57825e1a
child 52143 36ffe23b25f8
permissions -rw-r--r--
tuned proofs;
prensani@13020
     1
prensani@13020
     2
header {* \section{Concrete Syntax} *}
prensani@13020
     3
haftmann@16417
     4
theory Quote_Antiquote imports Main begin
prensani@13020
     5
prensani@13020
     6
syntax
prensani@13020
     7
  "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
prensani@13020
     8
  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
prensani@13020
     9
  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(.{_}.)" [0] 1000)
prensani@13020
    10
prensani@13020
    11
syntax (xsymbols)
prensani@13020
    12
  "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
prensani@13020
    13
prensani@13020
    14
translations
wenzelm@35107
    15
  ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
prensani@13020
    16
prensani@13020
    17
parse_translation {*
prensani@13020
    18
  let
wenzelm@42284
    19
    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
prensani@13020
    20
      | quote_tr ts = raise TERM ("quote_tr", ts);
wenzelm@35113
    21
  in [(@{syntax_const "_quote"}, quote_tr)] end
prensani@13020
    22
*}
prensani@13020
    23
prensani@13020
    24
end