--- 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}
*}
(*<*)