# HG changeset patch
# User wenzelm
# Date 1263299761 -3600
# Node ID d7786f56f081c5a53fcc497842cd9fc97d6c0c32
# Parent  ded5b770ec1cfb6a527572b8a28185dff7da78ab
recovered subscript (cf. ded5b770ec1c);

diff -r ded5b770ec1c -r d7786f56f081 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue Jan 12 09:59:45 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Tue Jan 12 13:36:01 2010 +0100
@@ -102,7 +102,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>8 @ term\<^isub>9 @ term\<^isub>10"}
+@{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}
 *}
diff -r ded5b770ec1c -r d7786f56f081 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Jan 12 09:59:45 2010 +0100
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Tue Jan 12 13:36:01 2010 +0100
@@ -130,7 +130,7 @@
 \isa{{\isacharat}}-terms to the left before printing, which leads to better
 line breaking behaviour:
 \begin{isabelle}%
-term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}{\isadigit{0}}%
+term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\isactrlisub {\isadigit{0}}%
 \end{isabelle}
 
 \end{itemize}%