--- a/doc-src/TutorialI/Types/types.tex Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Types/types.tex Wed Mar 07 15:54:11 2001 +0100
@@ -43,11 +43,11 @@
Isabelle offers the related concept of an \textbf{axiomatic type class}.
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
an axiomatic specification of a class of types. Thus we can talk about a type
-$t$ being in a class $c$, which is written $\tau :: c$. This is the case if
-$\tau$ satisfies the axioms of $c$. Furthermore, type classes can be
-organized in a hierarchy. Thus there is the notion of a class $d$ being a
-\textbf{subclass} of a class $c$, written $d < c$. This is the case if all
-axioms of $c$ are also provable in $d$. Let us now introduce these concepts
+$t$ being in a class $C$, which is written $\tau :: C$. This is the case if
+$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
+organized in a hierarchy. Thus there is the notion of a class $D$ being a
+\textbf{subclass} of a class $C$, written $D < C$. This is the case if all
+axioms of $C$ are also provable in $D$. We introduce these concepts
by means of a running example, ordering relations.
\subsection{Overloading}