--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy Mon Sep 21 10:58:25 2009 +0200
@@ -0,0 +1,24 @@
+
+header {* \section{Concrete Syntax} *}
+
+theory Quote_Antiquote imports Main begin
+
+syntax
+ "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
+ "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b" ("\<acute>_" [1000] 1000)
+ "_Assert" :: "'a \<Rightarrow> 'a set" ("(.{_}.)" [0] 1000)
+
+syntax (xsymbols)
+ "_Assert" :: "'a \<Rightarrow> 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
+
+translations
+ ".{b}." \<rightharpoonup> "Collect \<guillemotleft>b\<guillemotright>"
+
+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
\ No newline at end of file