author paulson Fri, 16 Feb 2001 18:51:19 +0100 changeset 11156 1d1d9f60c29b parent 11155 603df40ef1e9 child 11157 0d94005e374c
fixed the obvious errors Tobias found
--- 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}.