--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 17:39:29 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Sep 12 19:03:13 2000 +0200
@@ -69,19 +69,21 @@
rules for other higher-order functions on lists would look very similar but
have not been proved yet because they were never needed. If you get into a
situation where you need to supply \isacommand{recdef} with new congruence
-rules, you can either append the line
-\begin{ttbox}
-congs <congruence rules>
-\end{ttbox}
-to the specific occurrence of \isacommand{recdef} or declare them globally:
-\begin{ttbox}
-lemmas [????????] = <congruence rules>
-\end{ttbox}
-
-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.
+rules, you can either append a hint locally
+to the specific occurrence of \isacommand{recdef}%
+\end{isamarkuptext}%
+{\isacharparenleft}\isakeyword{hints}\ cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
+\begin{isamarkuptext}%
+\noindent
+or declare them globally
+by giving them the \isa{recdef{\isacharunderscore}cong} attribute as in%
+\end{isamarkuptext}%
+\isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
+\begin{isamarkuptext}%
+Note that the global \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
+intentionally kept apart because they control different activities, namely
+simplification and making recursive definitions. The local \isa{cong} in
+the hints section of \isacommand{recdef} is merely short for \isa{recdef{\isacharunderscore}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.%