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" ("(2\<lbrace>_,/ _\<rbrace>)") |
83 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
|
84 syntax_consts |
|
85 "_MTuple" == MPair |
84 translations |
86 translations |
85 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
87 "\<lbrace>x, y, z\<rbrace>" == "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
86 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" |
88 "\<lbrace>x, y\<rbrace>" == "CONST MPair x y" |
87 |
89 |
88 |
90 |