1.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Thu Oct 28 19:40:22 2004 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Oct 29 15:16:02 2004 +0200
     1.3 @@ -35,10 +35,9 @@
     1.4  We can either prove this as a separate lemma, or try to figure out which
     1.5  existing lemmas may help. We opt for the second alternative. The theory of
     1.6  lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs},
     1.7 -which is already
     1.8 -close to what we need, except that we still need to turn \mbox{\isa{{\isacharless}\ Suc}}
     1.9 +which is what we need, provided we turn \mbox{\isa{{\isacharless}\ Suc}}
    1.10  into
    1.11 -\isa{{\isasymle}} for the simplification rule to apply. Lemma
    1.12 +\isa{{\isasymle}} so that the rule applies. Lemma
    1.13  \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}.
    1.14  
    1.15  Now we retry the above definition but supply the lemma(s) just found (or

     2.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Thu Oct 28 19:40:22 2004 +0200
     2.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Oct 29 15:16:02 2004 +0200
     2.3 @@ -28,11 +28,10 @@
     2.4  @{text[display]"length (filter ... xs) < Suc (length xs)"}
     2.5  We can either prove this as a separate lemma, or try to figure out which
     2.6  existing lemmas may help. We opt for the second alternative. The theory of
     2.7 -lists contains the simplification rule @{thm length_filter[no_vars]},
     2.8 -which is already
     2.9 -close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
    2.10 +lists contains the simplification rule @{thm length_filter_le[no_vars]},
    2.11 +which is what we need, provided we turn \mbox{@{text"< Suc"}}
    2.12  into
    2.13 -@{text"\<le>"} for the simplification rule to apply. Lemma
    2.14 +@{text"\<le>"} so that the rule applies. Lemma
    2.15  @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
    2.16  
    2.17  Now we retry the above definition but supply the lemma(s) just found (or