new Union syntax
authorpaulson
Wed Feb 18 16:01:37 2004 +0100 (2004-02-18)
changeset 1439371dff3bade66
parent 14392 386760e88462
child 14394 51b24127eef2
new Union syntax
doc-src/TutorialI/Sets/sets.tex
     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