# HG changeset patch
# User wenzelm
# Date 1112858896 -7200
# Node ID 60c56561bcf481e3c3aea3c03b3e845883463d42
# Parent  32aea1e31eb8c8dea573d613357d3286bb922194
added term_8;

diff -r 32aea1e31eb8 -r 60c56561bcf4 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Apr 07 09:28:03 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Apr 07 09:28:16 2005 +0200
@@ -89,7 +89,7 @@
 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
 @{text"@"}-terms to the left before printing, which leads to better
 line breaking behaviour:
-@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
+@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
 
 \end{itemize}
 *}