doc-src/Codegen/Thy/Refinement.thy

 text {*
   \noindent The runtime of the corresponding code grows exponential due
   to two recursive calls:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts fib (consts) fib (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts fib (consts) fib (Haskell)}
 *}
 
 text {*
   \noindent A more efficient implementation would use dynamic
   programming, e.g.~sharing of common intermediate results between

 
 text {*
   \noindent The resulting code shows only linear growth of runtime:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts fib (consts) fib fib_step (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts fib (consts) fib fib_step (Haskell)}
 *}
 
 
 subsection {* Datatype refinement *}
 

 
 text {*
   \noindent The resulting code looks as expected:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts empty enqueue dequeue (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts empty enqueue dequeue (SML)}
 *}
 
 text {*
   The same techniques can also be applied to types which are not
   specified as datatypes, e.g.~type @{typ int} is originally specified

 
 text {*
   \noindent Then the corresponding code is as follows:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts Dlist.empty Dlist.insert Dlist.remove list_of_dlist (Haskell)}
 *} (*(types) dlist (consts) dempty dinsert dremove list_of List.member insert remove *)
 
 text {*
   Typical data structures implemented by representations involving
   invariants are available in the library, e.g.~theories @{theory