--- a/doc-src/TutorialI/Types/document/Overloading1.tex Sat Nov 04 18:54:22 2000 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Mon Nov 06 11:32:23 2000 +0100
@@ -2,8 +2,7 @@
\begin{isabellebody}%
\def\isabellecontext{Overloading{\isadigit{1}}}%
%
-\isamarkupsubsubsection{Controlled overloading with type classes%
-}
+\isamarkupsubsubsection{Controlled overloading with type classes}
%
\begin{isamarkuptext}%
We now start with the theory of ordering relations, which we want to phrase
@@ -26,6 +25,10 @@
\ \ \ \ \ \ \ le\ \ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequote}\ \ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequote}{\isacharless}{\isacharless}{\isacharequal}{\isachardoublequote}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}%
\begin{isamarkuptext}%
\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 \isa{ordrel}. To breathe life
into \isa{ordrel} we need to declare a type to be an \bfindex{instance} of
\isa{ordrel}:%