diff -r 1bece7f35762 -r 33fe2d701ddd doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:09:06 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Thu Oct 12 18:38:23 2000 +0200
@@ -66,10 +66,9 @@
 @{thm[display,margin=50]"map_cong"[no_vars]}
 Its second premise expresses (indirectly) that the second argument of
 @{term"map"} is only applied to elements of its third argument. Congruence
-rules for other higher-order functions on lists would look very similar but
-have not been proved yet because they were never needed. If you get into a
-situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append a hint locally
+rules for other higher-order functions on lists look very similar. If you get
+into a situation where you need to supply \isacommand{recdef} with new
+congruence rules, you can either append a hint locally
 to the specific occurrence of \isacommand{recdef}
 *}
 (*<*)