
diff -r ec3424dd17bc -r 69268a097405 doc-src/IsarRef/Thy/Outer_Syntax.thy
--- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:30:41 2008 +0100
+++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:31:25 2008 +0100
@@ -127,8 +127,9 @@
   "\<dots>"}~@{verbatim "*)"} and may be nested, although user-interface
   tools might prevent this.  Note that this form indicates source
   comments only, which are stripped after lexical analysis of the
-  input.  The Isar document syntax also provides formal comments that
-  are considered as part of the text (see \secref{sec:comments}).
+  input.  The Isar syntax also provides proper \emph{document
+  comments} that are considered as part of the text (see
+  \secref{sec:comments}).
 *}
 
 




