diff -r 5b6305cab436 -r 9feb1e0c4cb3 doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 15:43:15 2000 +0200
@@ -23,7 +23,6 @@
 @{term"trev"}:
 *};
 
-lemmas [cong] = map_cong;
 lemma "trev(trev t) = t";
 apply(induct_tac t rule:trev.induct);
 txt{*\noindent
@@ -32,12 +31,12 @@
 both of which are solved by simplification:
 *};
 
-by(simp_all add:rev_map sym[OF map_compose]);
+by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
 
 text{*\noindent
 If the proof of the induction step mystifies you, we recommend to go through
 the chain of simplification steps in detail; you will probably need the help of
-@{text"trace_simp"}.
+@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
 %\begin{quote}
 %{term[display]"trev(trev(App f ts))"}\\
 %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -84,5 +83,8 @@
 congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
 declaring a congruence rule for the simplifier does not make it
 available to \isacommand{recdef}, and vice versa. This is intentional.
+%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.
 *};
 (*<*)end;(*>*)