--- a/doc-src/TutorialI/Inductive/even-example.tex Tue Nov 19 10:41:20 2002 +0100
+++ b/doc-src/TutorialI/Inductive/even-example.tex Wed Nov 20 10:43:20 2002 +0100
@@ -186,8 +186,9 @@
\ 1.\ n\ \isasymin \ even\isanewline
\ 2.\ \isasymAnd na.\ \isasymlbrakk na\ \isasymin \ even;\ n\ \isasymin \ even\isasymrbrakk \ \isasymLongrightarrow \ n\ \isasymin \ even%
\end{isabelle}
-The first one is hopeless. Rule inductions involving
-non-trivial terms usually fail. How to deal with such situations
+The first one is hopeless. Rule induction on
+a non-variable term discards information, and usually fails.
+How to deal with such situations
in general is described in {\S}\ref{sec:ind-var-in-prems} below.
In the current case the solution is easy because
we have the necessary inverse, subtraction: