1.1 --- a/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 14:59:44 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 12 15:43:15 2000 +0200
     1.3 @@ -23,7 +23,6 @@
     1.4  @{term"trev"}:
     1.5  *};
     1.6  
     1.7 -lemmas [cong] = map_cong;
     1.8  lemma "trev(trev t) = t";
     1.9  apply(induct_tac t rule:trev.induct);
    1.10  txt{*\noindent
    1.11 @@ -32,12 +31,12 @@
    1.12  both of which are solved by simplification:
    1.13  *};
    1.14  
    1.15 -by(simp_all add:rev_map sym[OF map_compose]);
    1.16 +by(simp_all add:rev_map sym[OF map_compose] cong:map_cong);
    1.17  
    1.18  text{*\noindent
    1.19  If the proof of the induction step mystifies you, we recommend to go through
    1.20  the chain of simplification steps in detail; you will probably need the help of
    1.21 -@{text"trace_simp"}.
    1.22 +@{text"trace_simp"}. Theorem @{thm[source]map_cong} is discussed below.
    1.23  %\begin{quote}
    1.24  %{term[display]"trev(trev(App f ts))"}\\
    1.25  %{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
    1.26 @@ -84,5 +83,8 @@
    1.27  congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
    1.28  declaring a congruence rule for the simplifier does not make it
    1.29  available to \isacommand{recdef}, and vice versa. This is intentional.
    1.30 +%The simplifier's congruence rules cannot be used by recdef.
    1.31 +%For example the weak congruence rules for if and case would prevent
    1.32 +%recdef from generating sensible termination conditions.
    1.33  *};
    1.34  (*<*)end;(*>*)