doc-src/TutorialI/Sets/sets.tex

 \isa{\isasymexists z\isasymin A.\ P\ x}.  For indexed unions and
 intersections, you may see the constants 
 \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}
 
 \index{sets!finite}%

 \end{isabelle}
 A \textbf{bisimulation}\index{bisimulations} 
 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|)}