--- a/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jul 25 23:17:41 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex Tue Jul 25 23:17:42 2006 +0200
@@ -70,9 +70,10 @@
\item or a control symbol ``\verb,\,\verb,<^,\isa{ident}\verb,>,'', for example ``\verb,\,\verb,<^bold>,'',
-\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any printable ASCII
-character (excluding ``\verb,>,'') or non-ASCII character, for example
-``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
+\item or a raw control symbol ``\verb,\,\verb,<^raw:,\isa{{\isasymdots}}\verb,>,'' where ``\isa{{\isasymdots}}'' refers to any
+printable ASCII character (excluding ``\verb,.,'' and ``\verb,>,'') or
+non-ASCII character, for example ``\verb,\,\verb,<^raw:$\sum_{i =
+1}^n$>,'',
\item or a numbered raw control symbol ``\verb,\,\verb,<^raw,\isa{nnn}\verb,>, where \isa{nnn} are digits, for example
``\verb,\,\verb,<^raw42>,''.