--- a/doc-src/TutorialI/Sets/sets.tex Wed Mar 24 10:55:20 2004 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Wed Mar 24 10:55:38 2004 +0100
@@ -295,8 +295,8 @@
\index{union!indexed}%
Unions can be formed over the values of a given set. The syntax is
-\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
-x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
+\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or
+\isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
\begin{isabelle}
(b\ \isasymin\
(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x) =\ (\isasymexists x\isasymin A.\