diff -r 42671298f037 -r 313a24b66a8d doc-src/TutorialI/Protocol/document/Public.tex
--- a/doc-src/TutorialI/Protocol/document/Public.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Protocol/document/Public.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -24,10 +24,10 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{consts}\isamarkupfalse%
-\ pubK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
+\ pubK\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}agent\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
 \isacommand{abbreviation}\isamarkupfalse%
-\ priK\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}agent\ {\isasymRightarrow}\ key{\isachardoublequoteclose}\isanewline
-\isakeyword{where}\ {\isachardoublequoteopen}priK\ x\ \ {\isasymequiv}\ \ invKey{\isacharparenleft}pubK\ x{\isacharparenright}{\isachardoublequoteclose}%
+\ priK\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}agent\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ key{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}priK\ x\ \ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ \ invKey{\isaliteral{28}{\isacharparenleft}}pubK\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
 \begin{isamarkuptext}%
 \noindent
 The set \isa{bad} consists of those agents whose private keys are known to
@@ -40,8 +40,8 @@
 \isamarkuptrue%
 \isacommand{axioms}\isamarkupfalse%
 \isanewline
-\ \ inj{\isacharunderscore}pubK{\isacharcolon}\ \ \ \ \ \ \ \ {\isachardoublequoteopen}inj\ pubK{\isachardoublequoteclose}\isanewline
-\ \ priK{\isacharunderscore}neq{\isacharunderscore}pubK{\isacharcolon}\ \ \ {\isachardoublequoteopen}priK\ A\ {\isasymnoteq}\ pubK\ B{\isachardoublequoteclose}%
+\ \ inj{\isaliteral{5F}{\isacharunderscore}}pubK{\isaliteral{3A}{\isacharcolon}}\ \ \ \ \ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}inj\ pubK{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ priK{\isaliteral{5F}{\isacharunderscore}}neq{\isaliteral{5F}{\isacharunderscore}}pubK{\isaliteral{3A}{\isacharcolon}}\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}priK\ A\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ pubK\ B{\isaliteral{22}{\isachardoublequoteclose}}%
 \isadelimproof
 %
 \endisadelimproof