1.1 --- a/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 25 17:44:59 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Types/Overloading.thy	Wed Oct 25 18:24:33 2000 +0200
     1.3 @@ -3,8 +3,12 @@
     1.4  by intro_classes
     1.5  
     1.6  text{*\noindent
     1.7 -This means. Of course we should also define the meaning of @{text <<=} and
     1.8 -@{text <<} on lists.
     1.9 +This \isacommand{instance} declaration can be read like the declaration of
    1.10 +a function on types: the constructor @{text list} maps types of class @{text
    1.11 +term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
    1.12 +if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
    1.13 +Of course we should also define the meaning of @{text <<=} and
    1.14 +@{text <<} on lists:
    1.15  *}
    1.16  
    1.17  defs (overloaded)