# HG changeset patch
# User nipkow
# Date 1217426820 -7200
# Node ID 007a339b9e7d19c86e547cbfea50d12d8288afca
# Parent  5052736b8bccd8de4884fb5f61a99332f26f8c71
added hint about writing "x : set xs".

diff -r 5052736b8bcc -r 007a339b9e7d doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Wed Jul 30 07:34:01 2008 +0200
+++ b/doc-src/TutorialI/fp.tex	Wed Jul 30 16:07:00 2008 +0200
@@ -140,6 +140,14 @@
 more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
 $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
 always use HOL's predefined lists by building on theory \isa{Main}.
+\begin{warn}
+Looking ahead to sets and quanifiers in Part II:
+The best way to express that some element \isa{x} is in a list \isa{xs} is
+\isa{x $\in$ set xs}, where \isa{set} is a function that turns a list into the
+set of its elements.
+By the same device you can also write bounded quantifiers like
+\isa{$\forall$x $\in$ set xs} or embed lists in other set expressions.
+\end{warn}
 
 
 \subsection{The General Format}