diff -r 93d5408eb7d9 -r fbd097aec213 doc-src/TutorialI/Types/document/Overloading.tex
--- 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"