summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 20 Nov 2002 10:43:20 +0100 | |

changeset 13722 | e03747c2ca58 |

parent 13721 | 2cf506c09946 |

child 13723 | c7d104550205 |

textual tweak

--- 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: