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)
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
prensani@13020
    15
  ".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
prensani@13020
    16
prensani@13020
    17
parse_translation {*
prensani@13020
    18
  let
prensani@13020
    19
    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
prensani@13020
    20
      | quote_tr ts = raise TERM ("quote_tr", ts);
prensani@13020
    21
  in [("_quote", quote_tr)] end
prensani@13020
    22
*}
prensani@13020
    23
prensani@13020
    24
end