src/Doc/Classes/Classes.thy
changeset 69660 2bc2a8599369
parent 69597 ff784d5a5bfb
child 76987 4c275405faae
--- a/src/Doc/Classes/Classes.thy	Mon Jan 14 18:33:52 2019 +0000
+++ b/src/Doc/Classes/Classes.thy	Mon Jan 14 18:33:53 2019 +0000
@@ -588,14 +588,14 @@
 text \<open>
   \<^noindent> This maps to Haskell as follows:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (Haskell)}
 \<close>
 
 text \<open>
   \<^noindent> The code in SML has explicit dictionary passing:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (SML)}
 \<close>
 
@@ -603,7 +603,7 @@
 text \<open>
   \<^noindent> In Scala, implicits are used as dictionaries:
 \<close>
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts example (Scala)}
 \<close>