minor changes
Mon, 06 Nov 2000 16:43:01 +0100
changeset 10398 cdb451206ef9
parent 10397 e2d0dda41f2c
child 10399 e37e123738f7
minor changes
--- a/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 16:41:39 2000 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Mon Nov 06 16:43:01 2000 +0100
@@ -1,4 +1,3 @@
-% ID:         $Id$
 \chapter{Sets, Functions and Relations}
 Mathematics relies heavily on set theory: not just unions and intersections
@@ -633,7 +632,6 @@
 A \textbf{relation} is a set of pairs.  As such, the set operations apply
 to them.  For instance, we may form the union of two relations.  Other
@@ -728,10 +726,10 @@
-The \textbf{reflexive transitive closure} of a relation is particularly 
-important.  It has the postfix syntax \isa{r\isacharcircum{*}}.  The
-construction is defined   to be the least fixedpoint satisfying the
-following equation: 
+The \textbf{reflexive transitive closure} of the
+relation~\isa{r} is written with the
+postfix syntax \isa{r\isacharcircum{*}}.  It is the least solution of the
 r\isacharcircum{*}\ =\ Id\ \isasymunion\ (r\ O\ r\isacharcircum{*})
@@ -874,7 +872,6 @@
 \section{Well-founded relations and induction}
 Induction comes in many forms, including traditional mathematical 
 induction, structural induction on lists and induction on size. 
@@ -883,15 +880,13 @@
 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
 infinite  descending chains
 \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
-If $\prec$ is well-founded then it can be used with the \textbf{well-founded
-induction|see{induction, well-founded}} rule:
+If $\prec$ is well-founded then it can be used with the well-founded 
+induction rule: 
 \[ \infer{P(a)}{\infer*{P(x)}{[\forall y.\, y\prec x \imp P(y)]}} \]
 To show $P(a)$ for a particular term~$a$, it suffices to show $P(x)$ for
 arbitrary~$x$ under the assumption that $P(y)$ holds for $y\prec x$. 
 Intuitively, the well-foundedness of $\prec$ ensures that the chains of
-reasoning are finite.  For a fuller account of well-founded relations and
-induction see, for example, \cite{Baader-Nipkow}.
+reasoning are finite.
 In Isabelle, the induction rule is expressed like this:
@@ -1040,6 +1035,5 @@
 two agents in a process algebra is an example of coinduction.
 The coinduction rule can be strengthened in various ways; see 
 theory {\isa{Gfp}} for details.  
-An example using the fixed point operators appears later in this 
-chapter, in the section on computation tree logic
+This chapter ends with a case study concerning model checking for the
+temporal logic CTL\@.