diff -r 322475c2cb75 -r 894f845c3dbf doc-src/TutorialI/Inductive/document/Even.tex
--- a/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 06 10:24:44 2000 +0100
+++ b/doc-src/TutorialI/Inductive/document/Even.tex	Wed Dec 06 11:00:23 2000 +0100
@@ -31,7 +31,7 @@
 \rulename{even.step}
 
 \begin{isabelle}%
-\ \ \ \ \ 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%
+\ \ \ \ \ {\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%
 \end{isabelle}
 \rulename{even.induct}