1.1 --- a/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 25 17:44:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Overloading2.thy	Wed Oct 25 18:24:33 2000 +0200
     1.3 @@ -2,7 +2,9 @@
     1.4  
     1.5  text{*
     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 @{text ordrel} to permit their
    1.10 +comparison:
    1.11  *}
    1.12  
    1.13  instance list :: (ordrel)ordrel
    1.14 @@ -12,10 +14,8 @@
    1.15  le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
    1.16                size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
    1.17  
    1.18 -text{*
    1.19 +text{*\noindent
    1.20 +The infix function @{text"!"} yields the nth element of a list.
    1.21  %However, we retract the componetwise comparison of lists and return
    1.22 -
    1.23 -Note: only one definition because based on name.
    1.24 -*}
    1.25 -(*<*)end(*>*)
    1.26 -
    1.27 +%Note: only one definition because based on name.
    1.28 +*}(*<*)end(*>*)