--- a/doc-src/TutorialI/Sets/sets.tex Sat Mar 21 12:37:13 2009 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Sun Mar 22 19:36:04 2009 +0100
@@ -299,7 +299,7 @@
\isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
\begin{isabelle}
(b\ \isasymin\
-(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
+(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
b\ \isasymin\ B\ x)
\rulenamedx{UN_iff}
\end{isabelle}
@@ -414,12 +414,12 @@
$k$-element subsets of~$A$ is \index{binomial coefficients}
$\binom{n}{k}$.
-\begin{warn}
-The term \isa{finite\ A} is defined via a syntax translation as an
-abbreviation for \isa{A {\isasymin} Finites}, where the constant
-\cdx{Finites} denotes the set of all finite sets of a given type. There
-is no constant \isa{finite}.
-\end{warn}
+%\begin{warn}
+%The term \isa{finite\ A} is defined via a syntax translation as an
+%abbreviation for \isa{A {\isasymin} Finites}, where the constant
+%\cdx{Finites} denotes the set of all finite sets of a given type. There
+%is no constant \isa{finite}.
+%\end{warn}
\index{sets|)}