--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Oct 16 17:06:21 2007 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex Tue Oct 16 17:07:40 2007 +0200
@@ -260,7 +260,7 @@
\begin{isabelle}
\isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
\rulename{Suc_leI}\isanewline
-\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
+\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
\rulename{le_less_trans}
\end{isabelle}
%