diff -r cc1d4c3ca9db -r 7bba12c3b7b6 doc-src/TutorialI/Protocol/document/NS_Public.tex --- a/doc-src/TutorialI/Protocol/document/NS_Public.tex Wed Jan 27 14:03:08 2010 +0100 +++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex Tue Feb 02 09:48:20 2010 +0000 @@ -84,7 +84,7 @@ \begin{isabelle}% \ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}% \end{isabelle} -where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}. +where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}. Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not know who sent the message. Calling the trace variable \isa{evs{\isadigit{2}}} rather than simply \isa{evs} helps us know where we are in a proof after many