# HG changeset patch
# User wenzelm
# Date 1153862262 -7200
# Node ID eb529c6883ec8f0e55215947522cb95e997fd9c3
# Parent  7b2958d3d5754348d7bed68b7f2460f33e0e7edb
updated;

diff -r 7b2958d3d575 -r eb529c6883ec doc-src/IsarImplementation/Thy/document/prelim.tex
--- 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>,''.