diff -r d5ff8b782b29 -r fee7cfa69c50 src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -278,7 +278,7 @@
 text{*For proving @{text new_keys_not_used}*}
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X G));  X \<in> synth (analz H) |] 
-      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H"; 
+      ==> K \<in> keysFor (parts (G \<union> H)) | Key (invKey K) \<in> parts H" 
 by (force 
     dest!: parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
            analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD]