1.1 --- a/doc-src/TutorialI/Types/document/Overloading.tex	Thu Aug 09 10:17:45 2001 +0200
     1.2 +++ b/doc-src/TutorialI/Types/document/Overloading.tex	Thu Aug 09 18:12:15 2001 +0200
     1.3 @@ -6,7 +6,8 @@
     1.4  \begin{isamarkuptext}%
     1.5  \noindent
     1.6  This \isacommand{instance} declaration can be read like the declaration of
     1.7 -a function on types: the constructor \isa{list} maps types of class \isa{term}, i.e.\ all HOL types, to types of class \isa{ordrel}, i.e.\
     1.8 +a function on types.  The constructor \isa{list} maps types of class \isa{term} (all HOL types), to types of class \isa{ordrel};
     1.9 +in other words,
    1.10  if \isa{ty\ {\isacharcolon}{\isacharcolon}\ term} then \isa{ty\ list\ {\isacharcolon}{\isacharcolon}\ ordrel}.
    1.11  Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
    1.12  \isa{{\isacharless}{\isacharless}} on lists:%