--- 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}.