--- a/doc-src/TutorialI/Types/Overloading.thy Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/Overloading.thy Thu Aug 09 18:12:15 2001 +0200
@@ -4,8 +4,9 @@
text{*\noindent
This \isacommand{instance} declaration can be read like the declaration of
-a function on types: the constructor @{text list} maps types of class @{text
-term}, i.e.\ all HOL types, to types of class @{text ordrel}, i.e.\
+a function on types. The constructor @{text list} maps types of class @{text
+term} (all HOL types), to types of class @{text ordrel};
+in other words,
if @{text"ty :: term"} then @{text"ty list :: ordrel"}.
Of course we should also define the meaning of @{text <<=} and
@{text <<} on lists: