--- a/doc-src/TutorialI/Types/Overloading1.thy Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/Overloading1.thy Mon Nov 06 11:32:23 2000 +0100
@@ -26,6 +26,10 @@
le :: "('a::ordrel) \<Rightarrow> 'a \<Rightarrow> bool" (infixl "<<=" 50)
text{*\noindent
+Note that only one occurrence of a type variable in a type needs to be
+constrained with a class; the constraint is propagated to the other
+occurrences automatically.
+
So far there is not a single type of class @{text ordrel}. To breathe life
into @{text ordrel} we need to declare a type to be an \bfindex{instance} of
@{text ordrel}: