--- a/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:14:56 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Tue Dec 18 16:44:00 2001 +0100
@@ -387,9 +387,8 @@
\cdx{UNION} and \cdx{INTER}\@.
The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.
-We have only scratched the surface of Isabelle/HOL's set theory.
-Hundreds of theorems are proved in theory \isa{Set} and its
-descendants.
+We have only scratched the surface of Isabelle/HOL's set theory, which provides
+hundreds of theorems for your use.
\subsection{Finiteness and Cardinality}
@@ -1070,6 +1069,5 @@
is perhaps the best-known concept defined as a
greatest fixed point. Exhibiting a bisimulation to prove the equality of
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.
+The coinduction rule can be strengthened in various ways.
\index{fixed points|)}