diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -96,7 +96,7 @@
 \isacommand{by}\ blast
 \end{isabelle}
 %
-This is the same example using ASCII syntax, illustrating a pitfall: 
+This is the same example using \textsc{ascii} syntax, illustrating a pitfall: 
 \begin{isabelle}
 \isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)"
 \end{isabelle}
@@ -287,8 +287,8 @@
 \end{isabelle}
 
 Unions can be formed over the values of a given  set.  The syntax is
-\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN
-x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
+\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
+x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
 (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
@@ -320,12 +320,12 @@
 over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \
-({\isasymUnion}x.\ B\ x)\ {==}\
+({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
 ({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
 \end{isabelle}
 Abbreviations work as you might expect.  The term on the left-hand side of
 the
-\isa{==} symbol is automatically translated to the right-hand side when the
+\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
 term is parsed, the reverse translation being done when the term is
 displayed.
 
@@ -523,7 +523,7 @@
 
 Theorems involving these concepts can be hard to prove. The following 
 example is easy, but it cannot be proved automatically. To begin 
-with, we need a law that relates the quality of functions to 
+with, we need a law that relates the equality of functions to 
 equality over all arguments: 
 \begin{isabelle}
 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
@@ -535,7 +535,7 @@
 side of function composition: 
 \begin{isabelle}
 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
-\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline
+\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline
 \isacommand{apply}\ auto\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -593,7 +593,7 @@
 abbreviates an application of image to {\isa{UNIV}}: 
 \begin{isabelle}
 \ \ \ \ \ range\ f\
-{==}\ f`UNIV
+{\isasymrightleftharpoons}\ f`UNIV
 \end{isabelle}
 %
 Few theorems are proved specifically 
@@ -845,7 +845,7 @@
 Induction comes in many forms, including traditional mathematical 
 induction, structural induction on lists and induction on size. 
 More general than these is induction over a well-founded relation. 
-Such A relation expresses the notion of a terminating process. 
+Such a relation expresses the notion of a terminating process. 
 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. \]
@@ -944,9 +944,9 @@
 
 \section{Fixed Point Operators}
 
-Fixed point operators define sets recursively.  Most users invoke 
-them by making an inductive definition, as discussed in
-Chap.\ts\ref{chap:inductive} below.  However, they can be used directly.
+Fixed point operators define sets recursively.  They are invoked
+implicitly when making an inductive definition, as discussed in
+Chap.\ts\ref{chap:inductive} below.  However, they can be used directly, too.
 The
 \relax{least}  or \relax{strongest} fixed point yields an inductive
 definition;  the \relax{greatest} or \relax{weakest} fixed point yields a
@@ -954,7 +954,7 @@
 existence  of these fixed points is guaranteed by the Knaster-Tarski
 theorem. 
 
-The theory works applies only to monotonic functions. Isabelle's 
+The theory applies only to monotonic functions. Isabelle's 
 definition of monotone is overloaded over all orderings:
 \begin{isabelle}
 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%