diff -r 527811f00c56 -r 2f98365f57a8 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 16:10:24 2002 +0200
+++ b/doc-src/TutorialI/Sets/sets.tex	Wed Jul 31 17:42:38 2002 +0200
@@ -11,7 +11,7 @@
 function is a set, and the inverse image of a function maps sets to sets.
 
 This chapter will be useful to anybody who plans to develop a substantial
-proof.  sets are convenient for formalizing  computer science concepts such
+proof.  Sets are convenient for formalizing  computer science concepts such
 as grammars, logical calculi and state transition systems.  Isabelle can
 prove many statements involving sets automatically.
 
@@ -610,7 +610,7 @@
 general syntax for comprehension:
 \begin{isabelle}
 \isacommand{lemma}\ "f`A\ \isasymunion\ g`A\ =\ ({\isasymUnion}x{\isasymin}A.\ \isacharbraceleft f\ x,\ g\
-x\isacharbraceright)
+x\isacharbraceright)"
 \par\smallskip
 \isacommand{lemma}\ "f\ `\ \isacharbraceleft(x,y){.}\ P\ x\ y\isacharbraceright\ =\ \isacharbraceleft f(x,y)\ \isacharbar\ x\ y.\ P\ x\
 y\isacharbraceright"