--- a/doc-src/TutorialI/Protocol/protocol.tex Sun Aug 31 21:27:58 2003 +0200
+++ b/doc-src/TutorialI/Protocol/protocol.tex Mon Sep 01 15:07:43 2003 +0200
@@ -202,7 +202,7 @@
\isasymLongrightarrow\ Y\ \isasymin \ analz\ H"\isanewline
\ \ \ \ Decrypt\ [dest]:\ \isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ "{\isasymlbrakk}Crypt\ K\ X\ \isasymin \ analz\ H;\ Key(invKey\
-K):\ analz\ H\isasymrbrakk\isanewline
+K)\ \isasymin\ analz\ H\isasymrbrakk\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ X\ \isasymin \ analz\ H"
\end{isabelle}
%
@@ -306,8 +306,7 @@
of compromised users. After each \isa{Says} event, the spy learns the
message that was sent:
\begin{isabelle}
-\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ parts\
-\isacharbraceleft X\isacharbraceright \ \isasymunion\ (knows\ Spy\ evs)
+\ \ \ \ \ knows\ Spy\ ((Says\ A\ B\ X)\ \#\ evs)\ =\ insert X\ (knows\ Spy\ evs)
\end{isabelle}
%
Combinations of functions express other important