--- a/doc-src/TutorialI/Types/document/Overloading1.tex Tue May 01 17:16:32 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Tue May 01 22:26:55 2001 +0200
@@ -7,8 +7,8 @@
%
\begin{isamarkuptext}%
We now start with the theory of ordering relations, which we want to phrase
-in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}: they have
-been chosen to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
+in terms of the two binary symbols \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}}
+to avoid clashes with \isa{{\isacharless}} and \isa{{\isasymle}} in theory \isa{Main}. To restrict the application of \isa{{\isacharless}{\isacharless}} and \isa{{\isacharless}{\isacharless}{\isacharequal}} we
introduce the class \isa{ordrel}:%
\end{isamarkuptext}%
\isacommand{axclass}\ ordrel\ {\isacharless}\ {\isachardoublequote}term{\isachardoublequote}%
@@ -16,7 +16,7 @@
\noindent
This introduces a new class \isa{ordrel} and makes it a subclass of
the predefined class \isa{term}\footnote{The quotes around \isa{term}
-simply avoid the clash with the command \isacommand{term}.}; \isa{term}
+simply avoid the clash with the command \isacommand{term}.} --- \isa{term}
is the class of all HOL types, like ``Object'' in Java.
This is a degenerate form of axiomatic type class without any axioms.
Its sole purpose is to restrict the use of overloaded constants to meaningful