1.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Thu Jul 26 18:23:38 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Fri Aug 03 18:04:55 2001 +0200
     1.3 @@ -52,17 +52,18 @@
     1.4  where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
     1.5  name of a function that takes an $n$-tuple. Usually the subgoal will
     1.6  contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The
     1.7 -induction rules do not mention $f$ at all. For example @{thm[source]sep.induct}
     1.8 +induction rules do not mention $f$ at all. Here is @{thm[source]sep.induct}:
     1.9  \begin{isabelle}
    1.10  {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
    1.11  ~~{\isasymAnd}a~x.~P~a~[x];\isanewline
    1.12  ~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
    1.13  {\isasymLongrightarrow}~P~u~v%
    1.14  \end{isabelle}
    1.15 -merely says that in order to prove a property @{term"P"} of @{term"u"} and
    1.16 +It merely says that in order to prove a property @{term"P"} of @{term"u"} and
    1.17  @{term"v"} you need to prove it for the three cases where @{term"v"} is the
    1.18 -empty list, the singleton list, and the list with at least two elements
    1.19 -(in which case you may assume it holds for the tail of that list).
    1.20 +empty list, the singleton list, and the list with at least two elements.
    1.21 +The final case has an induction hypothesis:  you may assume that @{term"P"}
    1.22 +holds for the tail of that list.
    1.23  *}
    1.24  
    1.25  (*<*)