equal
deleted
inserted
replaced
79 |
79 |
80 (*<*) |
80 (*<*) |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
82 syntax |
82 syntax |
83 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)") |
83 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)") |
84 syntax_consts |
|
85 MPair |
|
86 translations |
84 translations |
87 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
85 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
88 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
86 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
89 |
87 |
90 |
88 |