diff -r 832c42be723e -r 7aef0e4a3aac doc-src/Classes/Thy/Classes.thy --- 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)} *}