Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/Inductive/even-example.tex
changeset 13722 e03747c2ca58
parent 12663 d33033205e2f 
--- 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:
isabelle