diff -r 578730810638 -r 887a15590f0e doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Wed Jun 07 14:19:10 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex	Wed Jun 07 14:19:48 2000 +0200
@@ -65,9 +65,9 @@
 
 The syntax of \texttt{string} admits any characters, including newlines;
 ``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) have to be escaped by
-a backslash.  Note that ML-style control characters are \emph{not} supported.
-The body of \texttt{verbatim} may consist of any text not containing
-``\verb|*}|''.
+a backslash; newlines need not be escaped.  Note that ML-style control
+characters are \emph{not} supported.  The body of \texttt{verbatim} may
+consist of any text not containing ``\verb|*}|''.
 
 Comments take the form \texttt{(*~\dots~*)} and may be
 nested\footnote{Proof~General may occasionally get confused by nested