1.1 --- a/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 13 17:43:33 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 13 17:46:49 2000 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4  \rulename{even.step}
     1.5  
     1.6  \begin{isabelle}%
     1.7 -\ \ \ \ \ {\isasymlbrakk}xa\ {\isasymin}\ even{\isacharsemicolon}\ P\ {\isadigit{0}}{\isacharsemicolon}\ {\isasymAnd}n{\isachardot}\ {\isasymlbrakk}n\ {\isasymin}\ even{\isacharsemicolon}\ P\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ xa%
     1.8 +\ \ \ \ \ xa\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ {\isadigit{0}}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ n\ {\isasymin}\ even\ {\isasymLongrightarrow}\ P\ n\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xa%
     1.9  \end{isabelle}
    1.10  \rulename{even.induct}
    1.11