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 %typewriter {*
+text %quotetypewriter {*
   @{code_stmts empty enqueue dequeue (SML)}
 *}
 
 text {*
   \noindent The @{command_def export_code} command takes a

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

 text {*
   \noindent The corresponding code in Haskell uses that language's
   native classes:
 *}
 
-text %quote %typewriter {*
+text %quotetypewriter {*
   @{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 %typewriter {*
+text %quotetypewriter {*
   @{code_stmts bexp (SML)}
 *}
 
 text {*
   \noindent Note the parameters with trailing underscore (@{verbatim