--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Tue Dec 07 18:10:13 2004 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Wed Dec 08 07:50:27 2004 +0100
@@ -6,7 +6,7 @@
section "Introduction"
-text{* This document is for those Isabelle users that have mastered
+text{* This document is for those Isabelle users who have mastered
the art of mixing \LaTeX\ text and Isabelle theories and never want to
typeset a theorem by hand anymore because they have experienced the
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
@@ -77,7 +77,7 @@
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
\item @{term"length xs"} instead of @{text"length xs"}.
-\item @{term"nth xs n"} instead of @{text"nth xs i"},
+\item @{term"nth xs n"} instead of @{text"nth xs n"},
the $n$th element of @{text xs}.
\item The @{text"@"} operation associates implicitly to the right,