author nipkow Fri, 06 Aug 2004 12:30:31 +0200 changeset 15115 1c3be9eb4126 parent 15114 70d1f5b7d0ad child 15116 af3bca62444b
Undid \Union syntax with subscripts.
--- 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)