diff -r ca8cd110f769 -r 2d6782e71702 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue May 07 14:28:34 2002 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue May 07 15:03:50 2002 +0200
@@ -64,7 +64,7 @@
 rules for other higher-order functions on lists are similar.  If you get
 into a situation where you need to supply \isacommand{recdef} with new
 congruence rules, you can append a hint after the end of
-the recursion equations:
+the recursion equations:\cmmdx{hints}
 *}
 (*<*)
 consts dummy :: "nat => nat"
@@ -84,8 +84,6 @@
 The @{text cong} and @{text recdef_cong} attributes are
 intentionally kept apart because they control different activities, namely
 simplification and making recursive definitions.
-% The local @{text cong} in
-% the hints section of \isacommand{recdef} is merely short for @{text recdef_cong}.
 %The simplifier's congruence rules cannot be used by recdef.
 %For example the weak congruence rules for if and case would prevent
 %recdef from generating sensible termination conditions.