# HG changeset patch
# User paulson
# Date 1062421663 -7200
# Node ID 04f905c13502d64a4da01e33df85aab289826ebb
# Parent  14a12da7288e4760deca73b8674fbfc17945ec20
Corrections due to John Matthews

diff -r 14a12da7288e -r 04f905c13502 doc-src/TutorialI/Protocol/Message.thy
--- 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*)
diff -r 14a12da7288e -r 04f905c13502 doc-src/TutorialI/Protocol/protocol.tex
--- 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
diff -r 14a12da7288e -r 04f905c13502 doc-src/TutorialI/Trie/document/Trie.tex
--- 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%
diff -r 14a12da7288e -r 04f905c13502 doc-src/TutorialI/preface.tex
--- 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,