src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author haftmann
Mon Sep 21 10:58:25 2009 +0200 (2009-09-21)
changeset 32621 a073cb249a06
parent 16417 src/HOL/HoareParallel/Quote_Antiquote.thy@9bc16273c2d4
child 35107 bdca9f765ee4
permissions -rw-r--r--
theory entry point for session Hoare_Parallel (now also with proper underscore)
     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> "Collect \<guillemotleft>b\<guillemotright>"
    16 
    17 parse_translation {*
    18   let
    19     fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
    20       | quote_tr ts = raise TERM ("quote_tr", ts);
    21   in [("_quote", quote_tr)] end
    22 *}
    23 
    24 end