doc-src/TutorialI/Recdef/document/Nested2.tex
changeset 10668 3b84288e60b7
parent 10654 458068404143
child 10696 76d7f6c9a14c
     1.1 --- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 13 17:43:33 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Wed Dec 13 17:46:49 2000 +0100
     1.3 @@ -61,8 +61,9 @@
     1.4  \isacommand{recdef} has been supplied with the congruence theorem
     1.5  \isa{map{\isacharunderscore}cong}:
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
     1.8 -\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
     1.9 +\ \ \ \ \ xs\ {\isacharequal}\ ys\ {\isasymLongrightarrow}\isanewline
    1.10 +\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isacharparenright}\ {\isasymLongrightarrow}\isanewline
    1.11 +\ \ \ \ \ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
    1.12  \end{isabelle}
    1.13  Its second premise expresses (indirectly) that the second argument of
    1.14  \isa{map} is only applied to elements of its third argument. Congruence