--- a/doc-src/TutorialI/Protocol/Message.thy Sun Aug 31 21:27:58 2003 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy Mon Sep 01 15:07:43 2003 +0200
@@ -94,7 +94,7 @@
Fst: "{|X,Y|} \<in> analz H ==> X \<in> analz H"
Snd: "{|X,Y|} \<in> analz H ==> Y \<in> analz H"
Decrypt [dest]:
- "[|Crypt K X \<in> analz H; Key(invKey K): analz H|] ==> X \<in> analz H"
+ "[|Crypt K X \<in> analz H; Key(invKey K) \<in> analz H|] ==> X \<in> analz H"
(*Monotonicity; Lemma 1 of Lowe's paper*)
--- 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
--- a/doc-src/TutorialI/Trie/document/Trie.tex Sun Aug 31 21:27:58 2003 +0200
+++ b/doc-src/TutorialI/Trie/document/Trie.tex Mon Sep 01 15:07:43 2003 +0200
@@ -175,7 +175,7 @@
Conceptually, each node contains a mapping from letters to optional
subtries. Above we have implemented this by means of an association
list. Replay the development replacing \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie{\isacharparenright}\ list}
- with \isa{{\isacharprime}a\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie\ option}.
+ with \isa{{\isacharprime}a\ {\isasymrightharpoonup}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ trie}.
\end{exercise}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/TutorialI/preface.tex Sun Aug 31 21:27:58 2003 +0200
+++ b/doc-src/TutorialI/preface.tex Mon Sep 01 15:07:43 2003 +0200
@@ -65,8 +65,8 @@
M{\"u}ller, Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto,
Cornelia Pusch, Norbert Schirmer and Martin Strecker. Stephan
Merz was also kind enough to read and comment on a draft version. We
-received comments from Stefano Bistarelli, Gergely Buday and Tanja
-Vos.
+received comments from Stefano Bistarelli, Gergely Buday, John Matthews
+and Tanja Vos.
The research has been funded by many sources, including the {\sc dfg} grants
Ni~491/2, Ni~491/3, Ni~491/4 and the {\sc epsrc} grants GR\slash K57381,