--- a/src/Doc/Tutorial/Protocol/Event.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy Tue Jan 16 09:30:00 2018 +0100
@@ -73,7 +73,7 @@
Says A B X => parts {X} \<union> used evs
| Gets A X => used evs
| Notes A X => parts {X} \<union> used evs)"
- \<comment>\<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
+ \<comment> \<open>The case for @{term Gets} seems anomalous, but @{term Gets} always
follows @{term Says} in real protocols. Seems difficult to change.
See @{text Gets_correct} in theory @{text "Guard/Extensions.thy"}.\<close>