doc-src/TutorialI/Sets/sets.tex
 changeset 14393 71dff3bade66 parent 13814 5402c2eaf393 child 14481 ab1e47451aaa
     1.1 --- a/doc-src/TutorialI/Sets/sets.tex	Wed Feb 18 10:40:29 2004 +0100
1.2 +++ b/doc-src/TutorialI/Sets/sets.tex	Wed Feb 18 16:01:37 2004 +0100
1.3 @@ -299,7 +299,7 @@
1.4  x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
1.5  \begin{isabelle}
1.6  (b\ \isasymin\
1.7 -(\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
1.8 +(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x) =\ (\isasymexists x\isasymin A.\
1.9  b\ \isasymin\ B\ x)
1.10  \rulenamedx{UN_iff}
1.11  \end{isabelle}
1.12 @@ -310,13 +310,11 @@
1.13  A;\ b\ \isasymin\
1.14  B\ a\isasymrbrakk\ \isasymLongrightarrow\
1.15  b\ \isasymin\
1.16 -({\isasymUnion}x\isasymin A.\
1.17 -B\ x)
1.18 +(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x)
1.19  \rulenamedx{UN_I}%
1.20  \isanewline
1.21  \isasymlbrakk b\ \isasymin\
1.22 -({\isasymUnion}x\isasymin A.\
1.23 -B\ x);\
1.24 +(\isasymUnion \isactrlbsub x\isasymin A\isactrlesub \ B\ x);\
1.25  {\isasymAnd}x.\ {\isasymlbrakk}x\ \isasymin\
1.26  A;\ b\ \isasymin\
1.27  B\ x\isasymrbrakk\ \isasymLongrightarrow\
1.28 @@ -329,7 +327,7 @@
1.29  \begin{isabelle}
1.30  \ \ \ \ \
1.31  ({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
1.32 -({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
1.33 +({\isasymUnion}\isactrlbsub x{\isasymin}UNIV\isactrlesub\ B\ x)
1.34  \end{isabelle}
1.35  %Abbreviations work as you might expect.  The term on the left-hand side of
1.36  %the \isasymrightleftharpoons\ symbol is automatically translated to the right-hand side when the
1.37 @@ -351,8 +349,7 @@
1.38  theorems are available:
1.39  \begin{isabelle}
1.40  (b\ \isasymin\
1.41 -({\isasymInter}x\isasymin A.\
1.42 -B\ x))\
1.43 +(\isasymInter \isactrlbsub x\isasymin A\isactrlesub \ B\ x))\
1.44  =\
1.45  ({\isasymforall}x\isasymin A.\
1.46  b\ \isasymin\ B\ x)
1.47 @@ -1071,3 +1068,7 @@
1.48  two agents in a process algebra is an example of coinduction.
1.49  The coinduction rule can be strengthened in various ways.
1.50  \index{fixed points|)}
1.51 +
1.52 +%The section "Case Study: Verified Model Checking" is part of this chapter
1.53 +\input{CTL/ctl}
1.54 +\endinput