doc-src/Classes/Thy/Classes.thy
changeset 39664 0afaf89ab591
parent 38812 e527a34bf69d
child 39680 a0d49ed5a23a
--- a/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 13:28:53 2010 +0200
+++ b/doc-src/Classes/Thy/Classes.thy	Thu Sep 23 15:46:17 2010 +0200
@@ -601,18 +601,31 @@
   \noindent This maps to Haskell as follows:
 *}
 (*<*)code_include %invisible Haskell "Natural" -(*>*)
-text %quote {*@{code_stmts example (Haskell)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (Haskell)}
+  \end{typewriter}
+*}
 
 text {*
   \noindent The code in SML has explicit dictionary passing:
 *}
-text %quote {*@{code_stmts example (SML)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (SML)}
+  \end{typewriter}
+*}
+
 
 text {*
   \noindent In Scala, implicts are used as dictionaries:
 *}
 (*<*)code_include %invisible Scala "Natural" -(*>*)
-text %quote {*@{code_stmts example (Scala)}*}
+text %quote {*
+  \begin{typewriter}
+    @{code_stmts example (Scala)}
+  \end{typewriter}
+*}
 
 
 subsection {* Inspecting the type class universe *}