doc-src/Codegen/Thy/Introduction.thy

 export_code %quote empty dequeue enqueue in SML
   module_name Example file "examples/example.ML"
 
 text {* \noindent resulting in the following code: *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts empty enqueue dequeue (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts empty enqueue dequeue (SML)}
 *}
 
 text {*
   \noindent The @{command_def export_code} command takes a
   space-separated list of constants for which code shall be generated;

 
 text {*
   \noindent This is the corresponding code:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts empty enqueue dequeue (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts empty enqueue dequeue (Haskell)}
 *}
 
 text {*
   \noindent For more details about @{command export_code} see
   \secref{sec:further}.

 text {*
   \noindent The corresponding code in Haskell uses that language's
   native classes:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts bexp (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts bexp (Haskell)}
 *}
 
 text {*
   \noindent This is a convenient place to show how explicit dictionary
   construction manifests in generated code -- the same example in
   @{text SML}:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts bexp (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts bexp (SML)}
 *}
 
 text {*
   \noindent Note the parameters with trailing underscore (@{verbatim
   "A_"}), which are the dictionary parameters.