diff -r f9f89b7cfdc7 -r 3f8ad7418e55 doc-src/TutorialI/Protocol/NS_Public.thy
--- a/doc-src/TutorialI/Protocol/NS_Public.thy	Wed Jul 11 10:52:20 2007 +0200
+++ b/doc-src/TutorialI/Protocol/NS_Public.thy	Wed Jul 11 10:53:39 2007 +0200
@@ -9,32 +9,31 @@
 
 theory NS_Public imports Public begin
 
-consts  ns_public  :: "event list set"
-
-inductive ns_public
-  intros
+inductive_set
+  ns_public :: "event list set"
+  where
          (*Initial trace is empty*)
    Nil:  "[] \<in> ns_public"
 
          (*The spy MAY say anything he CAN say.  We do not expect him to
            invent new nonces here, but he can also use NS1.  Common to
            all similar protocols.*)
-   Fake: "\<lbrakk>evs \<in> ns_public;  X \<in> synth (analz (knows Spy evs))\<rbrakk>
+ | Fake: "\<lbrakk>evs \<in> ns_public;  X \<in> synth (analz (knows Spy evs))\<rbrakk>
           \<Longrightarrow> Says Spy B X  # evs \<in> ns_public"
 
          (*Alice initiates a protocol run, sending a nonce to Bob*)
-   NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
+ | NS1:  "\<lbrakk>evs1 \<in> ns_public;  Nonce NA \<notin> used evs1\<rbrakk>
           \<Longrightarrow> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>)
                  # evs1  \<in>  ns_public"
 
          (*Bob responds to Alice's message with a further nonce*)
-   NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
+ | NS2:  "\<lbrakk>evs2 \<in> ns_public;  Nonce NB \<notin> used evs2;
            Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk>
           \<Longrightarrow> Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
                 # evs2  \<in>  ns_public"
 
          (*Alice proves her existence by sending NB back to Bob.*)
-   NS3:  "\<lbrakk>evs3 \<in> ns_public;
+ | NS3:  "\<lbrakk>evs3 \<in> ns_public;
            Says A  B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3;
            Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB, Agent B\<rbrace>)
               \<in> set evs3\<rbrakk>