diff -r 3ed58bbcf4bd -r 332347b9b942 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Mon Jul 16 13:14:19 2001 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Tue Jul 17 13:46:21 2001 +0200
@@ -324,7 +324,7 @@
 \rulenamedx{UN_E}
 \end{isabelle}
 %
-The following built-in syntax translation (see \S\ref{sec:def-translations})
+The following built-in syntax translation (see {\S}\ref{sec:def-translations})
 lets us express the union over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \
@@ -368,7 +368,7 @@
 Isabelle uses logical equivalences such as those above in automatic proof. 
 Unions, intersections and so forth are not simply replaced by their
 definitions.  Instead, membership tests are simplified.  For example,  $x\in
-A\cup B$ is replaced by $x\in A\vee x\in B$.
+A\cup B$ is replaced by $x\in A\lor x\in B$.
 
 The internal form of a comprehension involves the constant  
 \cdx{Collect},
@@ -742,7 +742,7 @@
 
 \subsection{The Reflexive and Transitive Closure}
 
-\index{closure!reflexive and transitive|(}%
+\index{reflexive and transitive closure|(}%
 The \textbf{reflexive and transitive closure} of the
 relation~\isa{r} is written with a
 postfix syntax.  In ASCII we write \isa{r\isacharcircum*} and in
@@ -871,7 +871,7 @@
 \isa{auto}, \isa{fast} and \isa{best}.  Section~\ref{sec:products} will discuss proof
 techniques for ordered pairs in more detail.
 \end{warn}
-\index{relations|)}\index{closure!reflexive and transitive|)}
+\index{relations|)}\index{reflexive and transitive closure|)}
 
 
 \section{Well-Founded Relations and Induction}
@@ -902,7 +902,7 @@
 complex recursive function definition or induction.  The induction rule
 returned by
 \isacommand{recdef} is good enough for most purposes.  We use an explicit
-well-founded induction only in \S\ref{sec:CTL-revisited}.
+well-founded induction only in {\S}\ref{sec:CTL-revisited}.
 \end{warn}
 
 Isabelle/HOL declares \cdx{less_than} as a relation object, 
@@ -960,11 +960,11 @@
 \end{isabelle}
 
 These constructions can be used in a
-\textbf{recdef} declaration (\S\ref{sec:recdef-simplification}) to define
+\textbf{recdef} declaration ({\S}\ref{sec:recdef-simplification}) to define
 the well-founded relation used to prove termination.
 
 The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library.  Baader and Nipkow \cite[\S2.5]{Baader-Nipkow}
+available in the Library.  Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow}
 discuss it. 
 
 \medskip
@@ -1014,7 +1014,7 @@
 
 \begin{warn}
 Casual readers should skip the rest of this section.  We use fixed point
-operators only in \S\ref{sec:VMC}.
+operators only in {\S}\ref{sec:VMC}.
 \end{warn}
 
 The theory applies only to monotonic functions.\index{monotone functions|bold} 
@@ -1065,7 +1065,8 @@
 gfp\ f%
 \rulename{coinduct}
 \end{isabelle}
-A \bfindex{bisimulation} is perhaps the best-known concept defined as a
+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