# HG changeset patch
# User paulson
# Date 1099055762 -7200
# Node ID 8b3f707a78a7c567fe8c51cfd99a921e56543605
# Parent  f856f4f3258fc3132176b9291694fd8ed32da1ce
fixed reference to renamed theorem

diff -r f856f4f3258f -r 8b3f707a78a7 doc-src/TutorialI/Recdef/document/termination.tex
--- a/doc-src/TutorialI/Recdef/document/termination.tex	Thu Oct 28 19:40:22 2004 +0200
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Oct 29 15:16:02 2004 +0200
@@ -35,10 +35,9 @@
 We can either prove this as a separate lemma, or try to figure out which
 existing lemmas may help. We opt for the second alternative. The theory of
 lists contains the simplification rule \isa{length\ {\isacharparenleft}filter\ P\ xs{\isacharparenright}\ {\isasymle}\ length\ xs},
-which is already
-close to what we need, except that we still need to turn \mbox{\isa{{\isacharless}\ Suc}}
+which is what we need, provided we turn \mbox{\isa{{\isacharless}\ Suc}}
 into
-\isa{{\isasymle}} for the simplification rule to apply. Lemma
+\isa{{\isasymle}} so that the rule applies. Lemma
 \isa{less{\isacharunderscore}Suc{\isacharunderscore}eq{\isacharunderscore}le} does just that: \isa{{\isacharparenleft}m\ {\isacharless}\ Suc\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}m\ {\isasymle}\ n{\isacharparenright}}.
 
 Now we retry the above definition but supply the lemma(s) just found (or
diff -r f856f4f3258f -r 8b3f707a78a7 doc-src/TutorialI/Recdef/termination.thy
--- a/doc-src/TutorialI/Recdef/termination.thy	Thu Oct 28 19:40:22 2004 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Oct 29 15:16:02 2004 +0200
@@ -28,11 +28,10 @@
 @{text[display]"length (filter ... xs) < Suc (length xs)"}
 We can either prove this as a separate lemma, or try to figure out which
 existing lemmas may help. We opt for the second alternative. The theory of
-lists contains the simplification rule @{thm length_filter[no_vars]},
-which is already
-close to what we need, except that we still need to turn \mbox{@{text"< Suc"}}
+lists contains the simplification rule @{thm length_filter_le[no_vars]},
+which is what we need, provided we turn \mbox{@{text"< Suc"}}
 into
-@{text"\<le>"} for the simplification rule to apply. Lemma
+@{text"\<le>"} so that the rule applies. Lemma
 @{thm[source]less_Suc_eq_le} does just that: @{thm less_Suc_eq_le[no_vars]}.
 
 Now we retry the above definition but supply the lemma(s) just found (or