--- a/doc-src/TutorialI/Types/document/Overloading.tex Sun Oct 21 19:48:19 2001 +0200
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Sun Oct 21 19:49:29 2001 +0200
@@ -1,8 +1,11 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading}%
+\isamarkupfalse%
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}{\isachardoublequote}term{\isachardoublequote}{\isacharparenright}ordrel\isanewline
-\isacommand{by}\ intro{\isacharunderscore}classes%
+\isamarkupfalse%
+\isacommand{by}\ intro{\isacharunderscore}classes\isamarkupfalse%
+%
\begin{isamarkuptext}%
\noindent
This \isacommand{instance} declaration can be read like the declaration of
@@ -12,11 +15,14 @@
Of course we should also define the meaning of \isa{{\isacharless}{\isacharless}{\isacharequal}} and
\isa{{\isacharless}{\isacharless}} on lists:%
\end{isamarkuptext}%
+\isamarkuptrue%
\isacommand{defs}\ {\isacharparenleft}\isakeyword{overloaded}{\isacharparenright}\isanewline
prefix{\isacharunderscore}def{\isacharcolon}\isanewline
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
-\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\end{isabellebody}%
+\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isamarkupfalse%
+\isamarkupfalse%
+\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"