1.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Fri Aug 25 12:17:09 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Mon Aug 28 09:32:51 2000 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4  The rest is pure simplification:
     1.5  *}
     1.6  
     1.7 -by auto;
     1.8 +by simp_all;
     1.9  
    1.10  text{*
    1.11  Try proving the above lemma by structural induction, and you find that you
    1.12 @@ -58,13 +58,13 @@
    1.13  contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
    1.14  induction rules do not mention $f$ at all. For example \isa{sep.induct}
    1.15  \begin{isabellepar}%
    1.16 -{\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline
    1.17 -~~{\isasymAnd}a~x.~?P~a~[x];\isanewline
    1.18 -~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
    1.19 -{\isasymLongrightarrow}~?P~?u~?v%
    1.20 +{\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline
    1.21 +~~{\isasymAnd}a~x.~P~a~[x];\isanewline
    1.22 +~~{\isasymAnd}a~x~y~zs.~P~a~(y~\#~zs)~{\isasymLongrightarrow}~P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
    1.23 +{\isasymLongrightarrow}~P~u~v%
    1.24  \end{isabellepar}%
    1.25 -merely says that in order to prove a property \isa{?P} of \isa{?u} and
    1.26 -\isa{?v} you need to prove it for the three cases where \isa{?v} is the
    1.27 +merely says that in order to prove a property \isa{P} of \isa{u} and
    1.28 +\isa{v} you need to prove it for the three cases where \isa{v} is the
    1.29  empty list, the singleton list, and the list with at least two elements
    1.30  (in which case you may assume it holds for the tail of that list).
    1.31  *}