doc-src/TutorialI/Misc/document/AdvancedInd.tex
changeset 25056 743f3603ba8b
parent 19654 2c02a8054616
child 25258 22d16596c306
     1.1 --- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 16 17:06:21 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Oct 16 17:07:40 2007 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4  \begin{isabelle}
     1.5  \isa{m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ Suc\ m\ {\isasymle}\ n}
     1.6  \rulename{Suc_leI}\isanewline
     1.7 -\isa{{\isasymlbrakk}i\ {\isasymle}\ j{\isacharsemicolon}\ j\ {\isacharless}\ k{\isasymrbrakk}\ {\isasymLongrightarrow}\ i\ {\isacharless}\ k}
     1.8 +\isa{{\isasymlbrakk}x\ {\isasymle}\ y{\isacharsemicolon}\ y\ {\isacharless}\ z{\isasymrbrakk}\ {\isasymLongrightarrow}\ x\ {\isacharless}\ z}
     1.9  \rulename{le_less_trans}
    1.10  \end{isabelle}
    1.11  %