diff -r d36864e3f06c -r a0d49ed5a23a doc-src/Classes/Thy/Classes.thy --- a/doc-src/Classes/Thy/Classes.thy Fri Sep 24 14:03:44 2010 +0200 +++ b/doc-src/Classes/Thy/Classes.thy Fri Sep 24 14:56:16 2010 +0200 @@ -601,19 +601,15 @@ \noindent This maps to Haskell as follows: *} (*<*)code_include %invisible Haskell "Natural" -(*>*) -text %quote {* - \begin{typewriter} - @{code_stmts example (Haskell)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts example (Haskell)} *} text {* \noindent The code in SML has explicit dictionary passing: *} -text %quote {* - \begin{typewriter} - @{code_stmts example (SML)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts example (SML)} *} @@ -621,10 +617,8 @@ \noindent In Scala, implicts are used as dictionaries: *} (*<*)code_include %invisible Scala "Natural" -(*>*) -text %quote {* - \begin{typewriter} - @{code_stmts example (Scala)} - \end{typewriter} +text %quote %typewriter {* + @{code_stmts example (Scala)} *}