--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Fri May 04 04:17:00 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Sun May 06 13:33:01 2007 +0200
@@ -90,6 +90,11 @@
\item @{term"nth xs n"} instead of @{text"nth xs n"},
the $n$th element of @{text xs}.
+\item Human readers are good at converting automatically from lists to
+sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
+becomes @{prop"x \<in> set xs"}.
+
\item The @{text"@"} operation associates implicitly to the right,
which leads to unpleasant line breaks if the term is too long for one
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Fri May 04 04:17:00 2007 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Sun May 06 13:33:01 2007 +0200
@@ -118,6 +118,11 @@
\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
the $n$th element of \isa{xs}.
+\item Human readers are good at converting automatically from lists to
+sets. Hence \texttt{OptionalSugar} contains syntax for supressing the
+conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}}
+becomes \isa{x\ {\isasymin}\ xs}.
+
\item The \isa{{\isacharat}} operation associates implicitly to the right,
which leads to unpleasant line breaks if the term is too long for one
line. To avoid this, \texttt{OptionalSugar} contains syntax to group