src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42284 326f57825e1a
child 52143 36ffe23b25f8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;


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> "CONST Collect \<guillemotleft>b\<guillemotright>"

parse_translation {*
  let
    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
      | quote_tr ts = raise TERM ("quote_tr", ts);
  in [(@{syntax_const "_quote"}, quote_tr)] end
*}

end