changeset 27712 007a339b9e7d
parent 27015 f8537d69f514
child 44048 64f574163ca2
--- 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}.
+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.
 \subsection{The General Format}