doc-src/Codegen/Thy/Foundations.thy

   which states that the given theorems should be considered as code
   equations for a @{text fun} statement -- the corresponding constant
   is determined syntactically.  The resulting code:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts dequeue (consts) dequeue (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts dequeue (consts) dequeue (Haskell)}
 *}
 
 text {*
   \noindent You may note that the equality test @{term "xs = []"} has
   been replaced by the predicate @{term "List.null xs"}.  This is due

   \noindent During preprocessing, the membership test is rewritten,
   resulting in @{const List.member}, which itself performs an explicit
   equality check, as can be seen in the corresponding @{text SML} code:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts collect_duplicates (SML)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts collect_duplicates (SML)}
 *}
 
 text {*
   \noindent Obviously, polymorphic equality is implemented the Haskell
   way using a type class.  How is this achieved?  HOL introduces an

 text {*
   \noindent In the corresponding code, there is no equation
   for the pattern @{term "AQueue [] []"}:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts strict_dequeue (consts) strict_dequeue (Haskell)}
 *}
 
 text {*
   \noindent In some cases it is desirable to have this
   pseudo-\qt{partiality} more explicitly, e.g.~as follows:

 text {*
   \noindent Then the code generator will just insert an error or
   exception at the appropriate position:
 *}
 
-text %quote {*
-  \begin{typewriter}
-    @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
-  \end{typewriter}
+text %quote %typewriter {*
+  @{code_stmts strict_dequeue' (consts) empty_queue strict_dequeue' (Haskell)}
 *}
 
 text {*
   \noindent This feature however is rarely needed in practice.  Note
   also that the HOL default setup already declares @{const undefined}