1.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 14:59:44 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 12 15:43:15 2000 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4  induction schema for type \isa{term} but the simpler one arising from
     1.5  \isa{trev}:%
     1.6  \end{isamarkuptext}%
     1.7 -\isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
     1.8  \isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
     1.9  \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
    1.10  \begin{isamarkuptxt}%
    1.11 @@ -29,12 +28,12 @@
    1.12  \end{isabelle}
    1.13  both of which are solved by simplification:%
    1.14  \end{isamarkuptxt}%
    1.15 -\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
    1.16 +\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
    1.17  \begin{isamarkuptext}%
    1.18  \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 -\isa{trace{\isacharunderscore}simp}.
    1.22 +\isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}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 @@ -82,7 +81,10 @@
    1.27  Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
    1.28  congruence rules as the simplifier (\S\ref{sec:simp-cong}) but that
    1.29  declaring a congruence rule for the simplifier does not make it
    1.30 -available to \isacommand{recdef}, and vice versa. This is intentional.%
    1.31 +available to \isacommand{recdef}, and vice versa. This is intentional.
    1.32 +%The simplifier's congruence rules cannot be used by recdef.
    1.33 +%For example the weak congruence rules for if and case would prevent
    1.34 +%recdef from generating sensible termination conditions.%
    1.35  \end{isamarkuptext}%
    1.36  \end{isabellebody}%
    1.37  %%% Local Variables: