doc-src/TutorialI/Protocol/document/Event.tex

--- a/doc-src/TutorialI/Protocol/document/Event.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Protocol/document/Event.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -466,7 +466,7 @@
 \emph{events}.  The most important event, \isa{Says\ A\ B\ X}, expresses
 $A\to B : X$, which is the attempt by~$A$ to send~$B$ the message~$X$.
 A trace is simply a list, constructed in reverse
-using~\isa{{\isacharhash}}.  Other event types include reception of messages (when
+using~\isa{{\isaliteral{23}{\isacharhash}}}.  Other event types include reception of messages (when
 we want to make it explicit) and an agent's storing a fact.
 
 Sometimes the protocol requires an agent to generate a new nonce. The
@@ -476,7 +476,7 @@
 The function \isa{used} has a straightforward
 recursive definition.  Here is the case for \isa{Says} event:
 \begin{isabelle}%
-\ \ \ \ \ used\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ parts\ {\isacharbraceleft}X{\isacharbraceright}\ {\isasymunion}\ used\ evs%
+\ \ \ \ \ used\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ parts\ {\isaliteral{7B}{\isacharbraceleft}}X{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ used\ evs%
 \end{isabelle}
 
 The function \isa{knows} formalizes an agent's knowledge.  Mostly we only
@@ -486,14 +486,14 @@
 of compromised users.  After each \isa{Says} event, the spy learns the
 message that was sent:
 \begin{isabelle}%
-\ \ \ \ \ knows\ Spy\ {\isacharparenleft}Says\ A\ B\ X\ {\isacharhash}\ evs{\isacharparenright}\ {\isacharequal}\ insert\ X\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}%
+\ \ \ \ \ knows\ Spy\ {\isaliteral{28}{\isacharparenleft}}Says\ A\ B\ X\ {\isaliteral{23}{\isacharhash}}\ evs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ X\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}%
 \end{isabelle}
 Combinations of functions express other important
 sets of messages derived from~\isa{evs}:
 \begin{itemize}
-\item \isa{analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}} is everything that the spy could
+\item \isa{analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}} is everything that the spy could
 learn by decryption
-\item \isa{synth\ {\isacharparenleft}analz\ {\isacharparenleft}knows\ Spy\ evs{\isacharparenright}{\isacharparenright}} is everything that the spy
+\item \isa{synth\ {\isaliteral{28}{\isacharparenleft}}analz\ {\isaliteral{28}{\isacharparenleft}}knows\ Spy\ evs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is everything that the spy
 could generate
 \end{itemize}%
 \end{isamarkuptext}%