--- a/doc-src/TutorialI/Types/Overloading2.thy Wed Oct 25 17:44:59 2000 +0200
+++ b/doc-src/TutorialI/Types/Overloading2.thy Wed Oct 25 18:24:33 2000 +0200
@@ -2,7 +2,9 @@
text{*
Of course this is not the only possible definition of the two relations.
-Componentwise
+Componentwise comparison of lists of equal length also makes sense. This time
+the elements of the list must also be of class @{text ordrel} to permit their
+comparison:
*}
instance list :: (ordrel)ordrel
@@ -12,10 +14,8 @@
le_list_def: "xs <<= (ys::'a::ordrel list) \<equiv>
size xs = size ys \<and> (\<forall>i<size xs. xs!i <<= ys!i)"
-text{*
+text{*\noindent
+The infix function @{text"!"} yields the nth element of a list.
%However, we retract the componetwise comparison of lists and return
-
-Note: only one definition because based on name.
-*}
-(*<*)end(*>*)
-
+%Note: only one definition because based on name.
+*}(*<*)end(*>*)