diff -r 1658fc9b2618 -r 747d36865c2c src/Doc/Tutorial/Protocol/Event.thy
--- a/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 23 16:41:14 2016 +0100
+++ b/src/Doc/Tutorial/Protocol/Event.thy	Tue Feb 23 17:47:23 2016 +0100
@@ -383,4 +383,4 @@
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)