diff -r 66d6da816be7 -r 2cf13a72e170 doc-src/TutorialI/Protocol/document/NS_Public.tex
--- 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