--- a/doc-src/TutorialI/Protocol/document/NS_Public.tex Sun Jun 08 14:30:46 2008 +0200
+++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Sun Jun 08 14:31:06 2008 +0200
@@ -384,7 +384,7 @@
\isaindent{{\isacharparenleft}}else\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ H{\isacharparenright}{\isacharparenright}\rulename{analz{\isacharunderscore}Crypt{\isacharunderscore}if}%
\end{isabelle}
The simplifier has also used \isa{Spy{\isacharunderscore}see{\isacharunderscore}priK}, proved in
-{\S}\ref{sec:regularity}) above, to yield \isa{Ba\ {\isasymin}\ bad}.
+{\S}\ref{sec:regularity} above, to yield \isa{Ba\ {\isasymin}\ bad}.
Recall that this subgoal concerns the case
where the last message to be sent was