# HG changeset patch
# User wenzelm
# Date 1153906375 -7200
# Node ID 96a4b3b7a6aadfbe5e2e0cfa07c4971aaf620dfc
# Parent  525f934b438b53be6e5839848790a439c5fedd29
updated;

diff -r 525f934b438b -r 96a4b3b7a6aa doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jul 26 11:32:50 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jul 26 11:32:55 2006 +0200
@@ -72,8 +72,7 @@
 
 \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$>,'',
+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>,''.