1.1 --- a/doc-src/TutorialI/Protocol/NS_Public.thy	Mon Feb 01 14:12:12 2010 +0100
     1.2 +++ b/doc-src/TutorialI/Protocol/NS_Public.thy	Tue Feb 02 09:49:07 2010 +0000
     1.3 @@ -76,7 +76,7 @@
     1.4  @{term [display,indent=5] "Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)"}
     1.5  may be extended by an event of the form
     1.6  @{term [display,indent=5] "Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)"}
     1.7 -where @{text NB} is a fresh nonce: @{term "Nonce NB \<in> used evs2"}.
     1.8 +where @{text NB} is a fresh nonce: @{term "Nonce NB \<notin> used evs2"}.
     1.9  Writing the sender as @{text A'} indicates that @{text B} does not 
    1.10  know who sent the message.  Calling the trace variable @{text evs2} rather
    1.11  than simply @{text evs} helps us know where we are in a proof after many

     2.1 --- a/doc-src/TutorialI/Protocol/document/NS_Public.tex	Mon Feb 01 14:12:12 2010 +0100
     2.2 +++ b/doc-src/TutorialI/Protocol/document/NS_Public.tex	Tue Feb 02 09:49:07 2010 +0000
     2.3 @@ -84,7 +84,7 @@
     2.4  \begin{isabelle}%
     2.5  \ \ \ \ \ Says\ B\ A\ {\isacharparenleft}Crypt\ {\isacharparenleft}pubK\ A{\isacharparenright}\ {\isasymlbrace}Nonce\ NA{\isacharcomma}\ Nonce\ NB{\isacharcomma}\ Agent\ B{\isasymrbrace}{\isacharparenright}%
     2.6  \end{isabelle}
     2.7 -where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymin}\ used\ evs{\isadigit{2}}}.
     2.8 +where \isa{NB} is a fresh nonce: \isa{Nonce\ NB\ {\isasymnotin}\ used\ evs{\isadigit{2}}}.
     2.9  Writing the sender as \isa{A{\isacharprime}} indicates that \isa{B} does not 
    2.10  know who sent the message.  Calling the trace variable \isa{evs{\isadigit{2}}} rather
    2.11  than simply \isa{evs} helps us know where we are in a proof after many