diff -r d3190c5a0e76 -r 175ccbd5415a doc-src/TutorialI/Recdef/document/Nested2.tex --- a/doc-src/TutorialI/Recdef/document/Nested2.tex Mon Dec 11 20:11:57 2000 +0100 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex Tue Dec 12 11:57:33 2000 +0100 @@ -61,9 +61,8 @@ \isacommand{recdef} has been supplied with the congruence theorem \isa{map{\isacharunderscore}cong}: \begin{isabelle}% -\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline -\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% +\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline +\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys% \end{isabelle} Its second premise expresses (indirectly) that the second argument of \isa{map} is only applied to elements of its third argument. Congruence