src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author wenzelm
Fri Apr 08 13:31:16 2011 +0200 (2011-04-08)
changeset 42284 326f57825e1a
parent 35113 1a0c129bb2e0
child 52143 36ffe23b25f8
permissions -rw-r--r--
explicit structure Syntax_Trans;
discontinued old-style constrainAbsC;
     1 
     2 header {* \section{Concrete Syntax} *}
     3 
     4 theory Quote_Antiquote imports Main begin
     5 
     6 syntax
     7   "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
     8   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
     9   "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(.{_}.)" [0] 1000)
    10 
    11 syntax (xsymbols)
    12   "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
    13 
    14 translations
    15   ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
    16 
    17 parse_translation {*
    18   let
    19     fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
    20       | quote_tr ts = raise TERM ("quote_tr", ts);
    21   in [(@{syntax_const "_quote"}, quote_tr)] end
    22 *}
    23 
    24 end