1.1 --- a/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Oct 25 17:44:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Types/document/Overloading2.tex	Wed Oct 25 18:24:33 2000 +0200
     1.3 @@ -4,7 +4,9 @@
     1.4  %
     1.5  \begin{isamarkuptext}%
     1.6  Of course this is not the only possible definition of the two relations.
     1.7 -Componentwise%
     1.8 +Componentwise comparison of lists of equal length also makes sense. This time
     1.9 +the elements of the list must also be of class \isa{ordrel} to permit their
    1.10 +comparison:%
    1.11  \end{isamarkuptext}%
    1.12  \isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}ordrel{\isacharparenright}ordrel\isanewline
    1.13  \isacommand{by}\ intro{\isacharunderscore}classes\isanewline
    1.14 @@ -13,11 +15,11 @@
    1.15  le{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ {\isasymequiv}\isanewline
    1.16  \ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
    1.17  \begin{isamarkuptext}%
    1.18 +\noindent
    1.19 +The infix function \isa{{\isacharbang}} yields the nth element of a list.
    1.20  %However, we retract the componetwise comparison of lists and return
    1.21 -
    1.22 -Note: only one definition because based on name.%
    1.23 +%Note: only one definition because based on name.%
    1.24  \end{isamarkuptext}%
    1.25 -\isanewline
    1.26  \end{isabellebody}%
    1.27  %%% Local Variables:
    1.28  %%% mode: latex