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