--- a/doc-src/Classes/Thy/Classes.thy Mon Sep 27 14:13:22 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy Mon Sep 27 16:19:36 2010 +0200
@@ -601,14 +601,14 @@
\noindent This maps to Haskell as follows:
*}
(*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Haskell)}
*}
text {*
\noindent The code in SML has explicit dictionary passing:
*}
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (SML)}
*}
@@ -617,7 +617,7 @@
\noindent In Scala, implicts are used as dictionaries:
*}
(*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote %typewriter {*
+text %quotetypewriter {*
@{code_stmts example (Scala)}
*}
--- a/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 14:13:22 2010 +0200
+++ b/doc-src/Classes/Thy/document/Classes.tex Mon Sep 27 16:19:36 2010 +0200
@@ -1123,11 +1123,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
module\ Example\ where\ {\isacharbraceleft}\isanewline
@@ -1195,23 +1195,23 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent The code in SML has explicit dictionary passing:%
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
structure\ Example\ {\isacharcolon}\ sig\isanewline
@@ -1295,12 +1295,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\begin{isamarkuptext}%
\noindent In Scala, implicts are used as dictionaries:%
@@ -1320,11 +1320,11 @@
%
\endisadeliminvisible
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
-\isatagtypewriter
+\isatagquotetypewriter
%
\begin{isamarkuptext}%
object\ Example\ {\isacharbraceleft}\isanewline
@@ -1398,12 +1398,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\endisatagtypewriter
-{\isafoldtypewriter}%
+\endisatagquotetypewriter
+{\isafoldquotetypewriter}%
%
-\isadelimtypewriter
+\isadelimquotetypewriter
%
-\endisadelimtypewriter
+\endisadelimquotetypewriter
%
\isamarkupsubsection{Inspecting the type class universe%
}