--- a/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Thu Aug 09 18:12:15 2001 +0200
@@ -54,7 +54,7 @@
Let us now return to the question of how \isacommand{recdef} can come up with
sensible termination conditions in the presence of higher-order functions
-like \isa{map}. For a start, if nothing were known about \isa{map},
+like \isa{map}. For a start, if nothing were known about \isa{map}, then
\isa{map\ trev\ ts} might apply \isa{trev} to arbitrary terms, and thus
\isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}. Therefore
\isacommand{recdef} has been supplied with the congruence theorem
@@ -63,22 +63,22 @@
\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
\isaindent{\ \ \ \ \ }{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
\end{isabelle}
-Its second premise expresses (indirectly) that the first argument of
-\isa{map} is only applied to elements of its second argument. Congruence
-rules for other higher-order functions on lists look very similar. If you get
+Its second premise expresses that in \isa{map\ f\ xs},
+function \isa{f} is only applied to elements of list \isa{xs}. Congruence
+rules for other higher-order functions on lists are similar. If you get
into a situation where you need to supply \isacommand{recdef} with new
-congruence rules, you can either append a hint after the end of
-the recursion equations%
+congruence rules, you can append a hint after the end of
+the recursion equations:%
\end{isamarkuptext}%
{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}cong{\isacharcolon}\ map{\isacharunderscore}cong{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
-or declare them globally
-by giving them the \attrdx{recdef_cong} attribute as in%
+Or you can declare them globally
+by giving them the \attrdx{recdef_cong} attribute:%
\end{isamarkuptext}%
\isacommand{declare}\ map{\isacharunderscore}cong{\isacharbrackleft}recdef{\isacharunderscore}cong{\isacharbrackright}%
\begin{isamarkuptext}%
-Note that the \isa{cong} and \isa{recdef{\isacharunderscore}cong} attributes are
+The \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