1.1 --- a/doc-src/TutorialI/Recdef/termination.thy Thu Oct 28 19:40:22 2004 +0200
1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri Oct 29 15:16:02 2004 +0200
1.3 @@ -28,11 +28,10 @@
1.4 @{text[display]"length (filter ... xs) < Suc (length xs)"}
1.5 We can either prove this as a separate lemma, or try to figure out which
1.6 existing lemmas may help. We opt for the second alternative. The theory of
1.7 -lists contains the simplification rule @{thm length_filter[no_vars]},
1.8 -which is already
1.9 -close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
1.10 +lists contains the simplification rule @{thm length_filter_le[no_vars]},
1.11 +which is what we need, provided we turn \mbox{@{text"< Suc"}}
1.12 into
1.13 -@{text"\<le>"} for the simplification rule to apply. Lemma
1.14 +@{text"\<le>"} so that the rule applies. Lemma
1.15 @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
1.16
1.17 Now we retry the above definition but supply the lemma(s) just found (or