src/Doc/Codegen/Refinement.thy

 text \<open>
   \noindent The runtime of the corresponding code grows exponential due
   to two recursive calls:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts fib (consts) fib (Haskell)}
 \<close>
 
 text \<open>
   \noindent A more efficient implementation would use dynamic

 
 text \<open>
   \noindent The resulting code shows only linear growth of runtime:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts fib (consts) fib fib_step (Haskell)}
 \<close>
 
 
 subsection \<open>Datatype refinement\<close>

 
 text \<open>
   \noindent The resulting code looks as expected:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
 \<close>
 
 text \<open>
   The same techniques can also be applied to types which are not

 
 text \<open>
   \noindent Then the corresponding code is as follows:
 \<close>
 
-text %quotetypewriter \<open>
+text %quote \<open>
   @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
 \<close>
 
 text \<open>
   See further @{cite "Haftmann-Kraus-Kuncar-Nipkow:2013:data_refinement"}