# HG changeset patch
# User nipkow
# Date 803727310 -7200
# Node ID e125fc7a11837a0dd0ab57aae6e21fb125b2f8a9
# Parent  57b5f55bf879f7838772fdb9fcc64f380b72aac4
Added remark that \...\ in strings is unnecessary.

diff -r 57b5f55bf879 -r e125fc7a1183 doc-src/Ref/theory-syntax.tex
--- 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}