Tuned.

--- a/doc-src/TutorialI/Protocol/Message.thy	Mon Jul 23 14:39:21 2007 +0200
+++ b/doc-src/TutorialI/Protocol/Message.thy	Mon Jul 23 15:04:56 2007 +0200
@@ -602,7 +602,7 @@
   | MPair  [intro]:
               "\<lbrakk>X \<in> synth H;  Y \<in> synth H\<rbrakk> \<Longrightarrow> \<lbrace>X,Y\<rbrace> \<in> synth H"
   | Crypt  [intro]:
-              "\<lbrakk>X \<in> synth H;  Key(K) \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
+              "\<lbrakk>X \<in> synth H;  Key K \<in> H\<rbrakk> \<Longrightarrow> Crypt K X \<in> synth H"
 (*<*)
 lemma synth_mono: "G\<subseteq>H ==> synth(G) \<subseteq> synth(H)"
   by (auto, erule synth.induct, auto)  

--- a/doc-src/TutorialI/Protocol/document/Message.tex	Mon Jul 23 14:39:21 2007 +0200
+++ b/doc-src/TutorialI/Protocol/document/Message.tex	Mon Jul 23 15:04:56 2007 +0200
@@ -1123,7 +1123,7 @@
 \ \ {\isacharbar}\ MPair\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Y\ {\isasymin}\ synth\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymlbrace}X{\isacharcomma}Y{\isasymrbrace}\ {\isasymin}\ synth\ H{\isachardoublequoteclose}\isanewline
 \ \ {\isacharbar}\ Crypt\ \ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\isanewline
-\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Key{\isacharparenleft}K{\isacharparenright}\ {\isasymin}\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ Crypt\ K\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}%
+\ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymlbrakk}X\ {\isasymin}\ synth\ H{\isacharsemicolon}\ \ Key\ K\ {\isasymin}\ H{\isasymrbrakk}\ {\isasymLongrightarrow}\ Crypt\ K\ X\ {\isasymin}\ synth\ H{\isachardoublequoteclose}%
 \isadelimproof
 %
 \endisadelimproof