diff -r 603df40ef1e9 -r 1d1d9f60c29b doc-src/TutorialI/Inductive/even-example.tex
--- a/doc-src/TutorialI/Inductive/even-example.tex	Fri Feb 16 18:50:09 2001 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex	Fri Feb 16 18:51:19 2001 +0100
@@ -142,8 +142,7 @@
 To conclude, we tell Isabelle that the desired value is
 \isa{Suc\ k}.  With this hint, the subgoal falls to \isa{simp}.
 \begin{isabelle}
-\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI, 
-\isacommand{apply}\ simp)
+\isacommand{apply}\ (rule_tac\ x\ =\ "Suc\ k"\ \isakeyword{in}\ exI, simp)
 \end{isabelle}
 
 
@@ -164,8 +163,8 @@
 Before applying induction, we typically must generalize
 the induction formula.  With rule induction, the required generalization
 can be hard to find and sometimes requires a complete reformulation of the
-problem.  In this  example, the obvious statement of the result is not
-inductive:
+problem.  In this  example, our first attempt uses the obvious statement of
+the result.  It fails:
 %
 \begin{isabelle}
 \isacommand{lemma}\ "Suc\ (Suc\ n)\ \isasymin \ even\
@@ -206,7 +205,7 @@
 Using our lemma, we can easily prove the result we originally wanted:
 \begin{isabelle}
 \isacommand{lemma}\ Suc_Suc_even_imp_even:\ "Suc\ (Suc\ n)\ \isasymin \ even\ \isasymLongrightarrow \ n\ \isasymin \ even"\isanewline
-\isacommand{by}\ (drule\ even_imp_even_minus_2, \isacommand{apply}\ simp)
+\isacommand{by}\ (drule\ even_imp_even_minus_2, simp)
 \end{isabelle}
 
 We have just proved the converse of the introduction rule \isa{even.step}.