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;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     1
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     2
header {* \section{Concrete Syntax} *}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     3
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 13020
diff changeset
     4
theory Quote_Antiquote imports Main begin
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     5
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     6
syntax
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     7
  "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     8
  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
     9
  "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(.{_}.)" [0] 1000)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    10
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    11
syntax (xsymbols)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    12
  "_Assert"    :: "'a \<Rightarrow> 'a set"            ("(\<lbrace>_\<rbrace>)" [0] 1000)
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    13
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    14
translations
35107
bdca9f765ee4 modernized translations;
wenzelm
parents: 32621
diff changeset
    15
  ".{b}." \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    16
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    17
parse_translation {*
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    18
  let
42284
326f57825e1a explicit structure Syntax_Trans;
wenzelm
parents: 35113
diff changeset
    19
    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    20
      | quote_tr ts = raise TERM ("quote_tr", ts);
35113
1a0c129bb2e0 modernized translations;
wenzelm
parents: 35107
diff changeset
    21
  in [(@{syntax_const "_quote"}, quote_tr)] end
13020
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    22
*}
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    23
791e3b4c4039 HoareParallel Theories
prensani
parents:
diff changeset
    24
end