# HG changeset patch
# User wenzelm
# Date 1226608285 -3600
# Node ID 69268a097405374529caa02f46d71bbe9393da9c
# Parent  ec3424dd17bc312701b83c09cb38013aa6bafba1
renamed "formal comments" to "document comments";

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}).
 *}