--- a/doc-src/TutorialI/Types/document/Overloading2.tex Thu Aug 09 10:17:45 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Thu Aug 09 18:12:15 2001 +0200
@@ -16,7 +16,13 @@
\ \ \ \ \ \ \ \ \ \ \ \ \ \ size\ xs\ {\isacharequal}\ size\ ys\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isacharless}size\ xs{\isachardot}\ xs{\isacharbang}i\ {\isacharless}{\isacharless}{\isacharequal}\ ys{\isacharbang}i{\isacharparenright}{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
-The infix function \isa{{\isacharbang}} yields the nth element of a list.%
+The infix function \isa{{\isacharbang}} yields the nth element of a list.
+
+\begin{warn}
+A type constructor can be instantiated in only one way to
+a given type class. For example, our two instantiations of \isa{list} must
+reside in separate theories with disjoint scopes.\REMARK{Tobias, please check}
+\end{warn}%
\end{isamarkuptext}%
%
\isamarkupsubsubsection{Predefined Overloading%
@@ -26,7 +32,7 @@
HOL comes with a number of overloaded constants and corresponding classes.
The most important ones are listed in Table~\ref{tab:overloading} in the appendix. They are
defined on all numeric types and sometimes on other types as well, for example
-\isa{{\isacharminus}}, \isa{{\isasymle}} and \isa{{\isacharless}} on sets.
+$-$ and \isa{{\isasymle}} on sets.
In addition there is a special input syntax for bounded quantifiers:
\begin{center}