equal
deleted
inserted
replaced
49 |
49 |
50 |
50 |
51 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
51 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
52 syntax |
52 syntax |
53 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>) |
53 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" (\<open>(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)\<close>) |
|
54 syntax_consts |
|
55 "_MTuple" \<rightleftharpoons> MPair |
54 translations |
56 translations |
55 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
57 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
56 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
58 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
57 |
59 |
58 |
60 |