doc-src/TutorialI/Protocol/document/Message.tex
changeset 42765 aec61b60ff7b
parent 40406 313a24b66a8d
child 43564 9864182c6bad
--- a/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 16:58:55 2011 +0200
+++ b/doc-src/TutorialI/Protocol/document/Message.tex	Thu May 12 17:17:57 2011 +0200
@@ -47,7 +47,7 @@
 the matching private key, and vice versa:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{types}\isamarkupfalse%
+\isacommand{type{\isaliteral{5F}{\isacharunderscore}}synonym}\isamarkupfalse%
 \ key\ {\isaliteral{3D}{\isacharequal}}\ nat\isanewline
 \isacommand{consts}\isamarkupfalse%
 \ invKey\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}key\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}%