doc-src/TutorialI/Protocol/document/NS_Public.tex
changeset 27094 2cf13a72e170
parent 23925 ee98c2528a8f
child 35503 7bba12c3b7b6
--- 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