diff -r 449e1a1bb7a8 -r d848c6693185 doc-src/TutorialI/Inductive/advanced-examples.tex
--- a/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Feb 16 00:36:21 2001 +0100
+++ b/doc-src/TutorialI/Inductive/advanced-examples.tex	Fri Feb 16 06:46:20 2001 +0100
@@ -65,7 +65,7 @@
 enlarging the set of function symbols enlarges the set of ground 
 terms. The proof is a trivial rule induction.
 First we use the \isa{clarify} method to assume the existence of an element of
-\isa{terms~F}.  (We could have used \isa{intro subsetI}.)  We then
+\isa{gterms~F}.  (We could have used \isa{intro subsetI}.)  We then
 apply rule induction. Here is the resulting subgoal: 
 \begin{isabelle}
 \ 1.\ \isasymAnd x\ args\ f.\isanewline
@@ -96,14 +96,14 @@
 Recall that \isa{even} is the minimal set closed under these two rules:
 \begin{isabelle}
 0\ \isasymin \ even\isanewline
-n\ \isasymin \ even\ \isasymLongrightarrow \ (Suc\ (Suc\ n))\ \isasymin
+n\ \isasymin \ even\ \isasymLongrightarrow \ Suc\ (Suc\ n)\ \isasymin
 \ even
 \end{isabelle}
 Minimality means that \isa{even} contains only the elements that these
 rules force it to contain.  If we are told that \isa{a}
 belongs to
 \isa{even} then there are only two possibilities.  Either \isa{a} is \isa{0}
-or else \isa{a} has the form \isa{Suc(Suc~n)}, for an arbitrary \isa{n}
+or else \isa{a} has the form \isa{Suc(Suc~n)}, for some suitable \isa{n}
 that belongs to
 \isa{even}.  That is the gist of the \isa{cases} rule, which Isabelle proves
 for us when it accepts an inductive definition: