# HG changeset patch
# User paulson
# Date 1080122138 -3600
# Node ID ab1e47451aaa88689c6ab644733e0b7e4420209c
# Parent  14b7923b3307bf6ee454577d26826576f173e31e
auto update

diff -r 14b7923b3307 -r ab1e47451aaa doc-src/TutorialI/Sets/sets.tex
--- 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.\