# HG changeset patch
# User paulson
# Date 1037785400 -3600
# Node ID e03747c2ca58406726a9afb63f8a57929a501fd5
# Parent  2cf506c09946eaa8b88313f65380a0ceb807a905
textual tweak

diff -r 2cf506c09946 -r e03747c2ca58 doc-src/TutorialI/Inductive/even-example.tex
--- 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: