# HG changeset patch
# User nipkow
# Date 1178451181 -7200
# Node ID bf67f798f063ae73052da547fd3c8fae099d3867
# Parent  51a16a7188209cb4ae1ecdfd7608d27b6736ea9b
added test about "set" supression

diff -r 51a16a718820 -r bf67f798f063 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- 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
diff -r 51a16a718820 -r bf67f798f063 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- 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