--- a/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/doc-src/TutorialI/Protocol/Message.thy Thu Feb 11 21:33:25 2010 +0100
@@ -82,14 +82,14 @@
(*<*)
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs