# HG changeset patch
# User wenzelm
# Date 1537725572 -7200
# Node ID d57c460ba11276a26a27c2be889c13b12ded1add
# Parent  e0d14f648d46c1361c3c00261fd1b5f41014efb9
tuned;

diff -r e0d14f648d46 -r d57c460ba112 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Sep 23 19:17:57 2018 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Sun Sep 23 19:59:32 2018 +0200
@@ -150,11 +150,10 @@
   blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
   of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
 
-  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although
-  the user-interface might prevent this. Note that this form indicates source
-  comments only, which are stripped after lexical analysis of the input. The
-  Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as
-  part of the text (see \secref{sec:comments}).
+  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested: the text is
+  removed after lexical analysis of the input and thus not suitable for
+  documentation. The Isar syntax also provides proper \<^emph>\<open>document comments\<close>
+  that are considered as part of the text (see \secref{sec:comments}).
 
   Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>.
   There are infinitely many Isabelle symbols like this, although proper