Added remark that \...\ in strings is unnecessary.

--- a/doc-src/Ref/theory-syntax.tex	Wed Jun 14 12:05:13 1995 +0200
+++ b/doc-src/Ref/theory-syntax.tex	Wed Jun 21 11:35:10 1995 +0200
@@ -10,9 +10,9 @@
 \item {\tt Typewriter font} denotes terminal symbols.
 \item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
   identifiers, type identifiers, natural numbers, \ML\ strings (with their
-  quotation marks) and arbitrary \ML\ text.  The first three are fully defined
-  in 
-\iflabelundefined{Defining-Logics}%
+  quotation marks, but without the need for \verb$\$ at the end of a line and
+  the beginning of the next line) and arbitrary \ML\ text.  The first three
+  are fully defined in \iflabelundefined{Defining-Logics}%
     {{\it The Isabelle Reference Manual}, chapter `Defining Logics'}%
     {Chap.\ts\ref{Defining-Logics}}.
 \end{itemize}