--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 14:59:44 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 15:43:15 2000 +0200
@@ -17,7 +17,6 @@
induction schema for type \isa{term} but the simpler one arising from
\isa{trev}:%
\end{isamarkuptext}%
-\isacommand{lemmas}\ {\isacharbrackleft}cong{\isacharbrackright}\ {\isacharequal}\ map{\isacharunderscore}cong\isanewline
\isacommand{lemma}\ {\isachardoublequote}trev{\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ t\ rule{\isacharcolon}trev{\isachardot}induct{\isacharparenright}%
\begin{isamarkuptxt}%
@@ -29,12 +28,12 @@
\end{isabelle}
both of which are solved by simplification:%
\end{isamarkuptxt}%
-\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
+\isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}\ cong{\isacharcolon}map{\isacharunderscore}cong{\isacharparenright}%
\begin{isamarkuptext}%
\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
-\isa{trace{\isacharunderscore}simp}.
+\isa{trace{\isacharunderscore}simp}. Theorem \isa{map{\isacharunderscore}cong} is discussed below.
%\begin{quote}
%{term[display]"trev(trev(App f ts))"}\\
%{term[display]"App f (rev(map trev (rev(map trev ts))))"}\\
@@ -82,7 +81,10 @@
Note that \isacommand{recdef} feeds on exactly the same \emph{kind} of
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.%
+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{isamarkuptext}%
\end{isabellebody}%
%%% Local Variables: