1.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Tue Feb 10 12:02:11 2004 +0100
     1.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Tue Feb 10 12:17:04 2004 +0100
     1.3 @@ -307,8 +307,8 @@
     1.4  \noindent The datatype induction rule generated here is of the form
     1.5    \begin{isabelle}%
     1.6  \ {\isasymlbrakk}P\ Leaf{\isacharsemicolon}\isanewline
     1.7 -\isaindent{\ \ \ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
     1.8 -\isaindent{\ \ \ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
     1.9 +\isaindent{\ \ }{\isasymAnd}a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isachardot}\isanewline
    1.10 +\isaindent{\ \ \ \ \ }{\isasymlbrakk}P\ bintree{\isadigit{1}}{\isacharsemicolon}\ P\ bintree{\isadigit{2}}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Branch\ a\ bintree{\isadigit{1}}\ bintree{\isadigit{2}}{\isacharparenright}{\isasymrbrakk}\isanewline
    1.11  \isaindent{\ }{\isasymLongrightarrow}\ P\ bintree%
    1.12  \end{isabelle}%
    1.13  \end{isamarkuptext}%