diff -r 368414099877 -r a5604ff1ef4e doc-src/TutorialI/Sets/sets.tex
--- 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|)}