--- a/doc-src/TutorialI/Sets/sets.tex Wed Feb 18 10:40:29 2004 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Wed Feb 18 16:01:37 2004 +0100
@@ -299,7 +299,7 @@
x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
\begin{isabelle}
(b\ \isasymin\
-(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x) =\ (\isasymexists x\isasymin A.\
b\ \isasymin\ B\ x)
\rulenamedx{UN_iff}
\end{isabelle}
@@ -310,13 +310,11 @@
A;\ b\ \isasymin\
B\ a\isasymrbrakk\ \isasymLongrightarrow\
b\ \isasymin\
-({\isasymUnion}x\isasymin A.\
-B\ x)
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x)
\rulenamedx{UN_I}%
\isanewline
\isasymlbrakk b\ \isasymin\
-({\isasymUnion}x\isasymin A.\
-B\ x);\
+(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x);\
{\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
A;\ b\ \isasymin\
B\ x\isasymrbrakk\ \isasymLongrightarrow\
@@ -329,7 +327,7 @@
\begin{isabelle}
\ \ \ \ \
({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
-({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
+({\isasymUnion}\isactrlbsub x{\isasymin}UNIV\isactrlesub\ 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
@@ -351,8 +349,7 @@
theorems are available:
\begin{isabelle}
(b\ \isasymin\
-({\isasymInter}x\isasymin A.\
-B\ x))\
+(\isasymInter \isactrlbsub x\isasymin A\isactrlesub \ B\ x))\
=\
({\isasymforall}x\isasymin A.\
b\ \isasymin\ B\ x)
@@ -1071,3 +1068,7 @@
two agents in a process algebra is an example of coinduction.
The coinduction rule can be strengthened in various ways.
\index{fixed points|)}
+
+%The section "Case Study: Verified Model Checking" is part of this chapter
+\input{CTL/ctl}
+\endinput