--- 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]