# HG changeset patch
# User paulson
# Date 1077116497 -3600
# Node ID 71dff3bade664cdb3e5ec76bc10bac9466ae9f7e
# Parent  386760e884626e5cd9b0711b69d90a4a1694331d
new Union syntax

diff -r 386760e88462 -r 71dff3bade66 doc-src/TutorialI/Sets/sets.tex
--- 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