doc-src/TutorialI/Protocol/document/NS_Public.tex

 {\isacharparenleft}if\ Key\ {\isacharparenleft}invKey\ K{\isacharparenright}\ {\isasymin}\ analz\ H\isanewline
 \isaindent{{\isacharparenleft}}then\ insert\ {\isacharparenleft}Crypt\ K\ X{\isacharparenright}\ {\isacharparenleft}analz\ {\isacharparenleft}insert\ X\ H{\isacharparenright}{\isacharparenright}\isanewline
 \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
 \[ 1.\quad  A'\to B'  : \comp{Na',A'}\sb{Kb'}. \]
 This message can compromise $Nb$ only if $Nb=Na'$ and $B'$ is compromised,