diff -r 51451d73c3d4 -r 9e59b4c11039 doc-src/TutorialI/Protocol/Event.thy
--- a/doc-src/TutorialI/Protocol/Event.thy	Thu Sep 30 08:50:45 2010 +0200
+++ b/doc-src/TutorialI/Protocol/Event.thy	Thu Sep 30 09:31:07 2010 +0200
@@ -23,24 +23,15 @@
        
 consts 
   bad    :: "agent set"                         -- {* compromised agents *}
-  knows  :: "agent => event list => msg set"
 
 
 text{*The constant "spies" is retained for compatibility's sake*}
 
-abbreviation (input)
-  spies  :: "event list => msg set" where
-  "spies == knows Spy"
-
-text{*Spy has access to his own key for spoof messages, but Server is secure*}
-specification (bad)
-  Spy_in_bad     [iff]: "Spy \<in> bad"
-  Server_not_bad [iff]: "Server \<notin> bad"
-    by (rule exI [of _ "{Spy}"], simp)
-
 primrec
+  knows :: "agent => event list => msg set"
+where
   knows_Nil:   "knows A [] = initState A"
-  knows_Cons:
+| knows_Cons:
     "knows A (ev # evs) =
        (if A = Spy then 
         (case ev of
@@ -57,20 +48,29 @@
          | Notes A' X    => 
              if A'=A then insert X (knows A evs) else knows A evs))"
 
+abbreviation (input)
+  spies  :: "event list => msg set" where
+  "spies == knows Spy"
+
+text{*Spy has access to his own key for spoof messages, but Server is secure*}
+specification (bad)
+  Spy_in_bad     [iff]: "Spy \<in> bad"
+  Server_not_bad [iff]: "Server \<notin> bad"
+    by (rule exI [of _ "{Spy}"], simp)
+
 (*
   Case A=Spy on the Gets event
   enforces the fact that if a message is received then it must have been sent,
   therefore the oops case must use Notes
 *)
 
-consts
+primrec
   (*Set of items that might be visible to somebody:
     complement of the set of fresh items*)
   used :: "event list => msg set"
-
-primrec
+where
   used_Nil:   "used []         = (UN B. parts (initState B))"
-  used_Cons:  "used (ev # evs) =
+| used_Cons:  "used (ev # evs) =
                      (case ev of
                         Says A B X => parts {X} \<union> used evs
                       | Gets A X   => used evs