# HG changeset patch
# User wenzelm
# Date 1153906370 -7200
# Node ID 525f934b438b53be6e5839848790a439c5fedd29
# Parent  2b319e94590561ffcf5f968142a31f25e26a353b
fixed LaTeX problem;

diff -r 2b319e945905 -r 525f934b438b doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jul 26 10:09:25 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jul 26 11:32:50 2006 +0200
@@ -49,8 +49,7 @@
 \item or a raw control symbol ``\verb,\,\verb,<^raw:,@{text
 "\<dots>"}\verb,>,'' where ``@{text "\<dots>"}'' 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,@{text
 "nnn"}\verb,>, where @{text "nnn"} are digits, for example