1.1 --- a/doc-src/TutorialI/Sets/sets.tex	Thu Aug 05 10:51:30 2004 +0200
     1.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Fri Aug 06 12:30:31 2004 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4  \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
     1.5  \begin{isabelle}
     1.6  (b\ \isasymin\
     1.7 -(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x) =\ (\isasymexists x\isasymin A.\
     1.8 +(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
     1.9  b\ \isasymin\ B\ x)
    1.10  \rulenamedx{UN_iff}
    1.11  \end{isabelle}
    1.12 @@ -310,11 +310,11 @@
    1.13  A;\ b\ \isasymin\
    1.14  B\ a\isasymrbrakk\ \isasymLongrightarrow\
    1.15  b\ \isasymin\
    1.16 -(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x)
    1.17 +(\isasymUnion x\isasymin A. B\ x)
    1.18  \rulenamedx{UN_I}%
    1.19  \isanewline
    1.20  \isasymlbrakk b\ \isasymin\
    1.21 -(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x);\
    1.22 +(\isasymUnion x\isasymin A. B\ x);\
    1.23  {\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
    1.24  A;\ b\ \isasymin\
    1.25  B\ x\isasymrbrakk\ \isasymLongrightarrow\
    1.26 @@ -327,7 +327,7 @@
    1.27  \begin{isabelle}
    1.28  \ \ \ \ \
    1.29  ({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
    1.30 -({\isasymUnion}\isactrlbsub x{\isasymin}UNIV\isactrlesub\ B\ x)
    1.31 +({\isasymUnion}x{\isasymin}UNIV. B\ x)
    1.32  \end{isabelle}
    1.33  %Abbreviations work as you might expect.  The term on the left-hand side of
    1.34  %the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
    1.35 @@ -349,7 +349,7 @@
    1.36  theorems are available:
    1.37  \begin{isabelle}
    1.38  (b\ \isasymin\
    1.39 -(\isasymInter \isactrlbsub x\isasymin A\isactrlesub \ B\ x))\
    1.40 +(\isasymInter x\isasymin A. B\ x))\
    1.41  =\
    1.42  ({\isasymforall}x\isasymin A.\
    1.43  b\ \isasymin\ B\ x)