# HG changeset patch
# User nipkow
# Date 1091788231 -7200
# Node ID 1c3be9eb41265c8aa3a31effadf019b99e6772d1
# Parent  70d1f5b7d0ad2d3385d91629a70ff17e503dde8b
Undid \Union syntax with subscripts.

diff -r 70d1f5b7d0ad -r 1c3be9eb4126 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Thu Aug 05 10:51:30 2004 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Aug 06 12:30:31 2004 +0200
@@ -299,7 +299,7 @@
 \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.\
+(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{UN_iff}
 \end{isabelle}
@@ -310,11 +310,11 @@
 A;\ b\ \isasymin\
 B\ a\isasymrbrakk\ \isasymLongrightarrow\
 b\ \isasymin\
-(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x)
+(\isasymUnion x\isasymin A. B\ x)
 \rulenamedx{UN_I}%
 \isanewline
 \isasymlbrakk b\ \isasymin\
-(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x);\
+(\isasymUnion x\isasymin A. B\ x);\
 {\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
 A;\ b\ \isasymin\
 B\ x\isasymrbrakk\ \isasymLongrightarrow\
@@ -327,7 +327,7 @@
 \begin{isabelle}
 \ \ \ \ \
 ({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
-({\isasymUnion}\isactrlbsub x{\isasymin}UNIV\isactrlesub\ B\ x)
+({\isasymUnion}x{\isasymin}UNIV. B\ x)
 \end{isabelle}
 %Abbreviations work as you might expect.  The term on the left-hand side of
 %the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
@@ -349,7 +349,7 @@
 theorems are available:
 \begin{isabelle}
 (b\ \isasymin\
-(\isasymInter \isactrlbsub x\isasymin A\isactrlesub \ B\ x))\
+(\isasymInter x\isasymin A. B\ x))\
 =\
 ({\isasymforall}x\isasymin A.\
 b\ \isasymin\ B\ x)