diff -r f075640b8868 -r 3abf6a722518 src/Doc/Tutorial/Documents/Documents.thy
--- a/src/Doc/Tutorial/Documents/Documents.thy	Tue Jan 16 09:12:16 2018 +0100
+++ b/src/Doc/Tutorial/Documents/Documents.thy	Tue Jan 16 09:30:00 2018 +0100
@@ -484,9 +484,9 @@
 \<close>
 
 lemma "A --> A"
-  \<comment> "a triviality of propositional logic"
-  \<comment> "(should not really bother)"
-  by (rule impI) \<comment> "implicit assumption step involved here"
+  \<comment> \<open>a triviality of propositional logic\<close>
+  \<comment> \<open>(should not really bother)\<close>
+  by (rule impI) \<comment> \<open>implicit assumption step involved here\<close>
 
 text \<open>
   \noindent The above output has been produced as follows: