doc-src/Codegen/Thy/Adaptation.thy
changeset 39664 0afaf89ab591
parent 39643 29cc021398fc
child 39683 f75a01ee6c41
     1.1 --- a/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 13:28:53 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 15:46:17 2010 +0200
     1.3 @@ -175,7 +175,11 @@
     1.4  code_const %invisible True and False and "op \<and>" and Not
     1.5    (SML and and and)
     1.6  (*>*)
     1.7 -text %quote {*@{code_stmts in_interval (SML)}*}
     1.8 +text %quote {*
     1.9 +  \begin{typewriter}
    1.10 +    @{code_stmts in_interval (SML)}
    1.11 +  \end{typewriter}
    1.12 +*}
    1.13  
    1.14  text {*
    1.15    \noindent Though this is correct code, it is a little bit
    1.16 @@ -204,7 +208,11 @@
    1.17    placeholder for the type constructor's (the constant's) arguments.
    1.18  *}
    1.19  
    1.20 -text %quote {*@{code_stmts in_interval (SML)}*}
    1.21 +text %quote {*
    1.22 +  \begin{typewriter}
    1.23 +    @{code_stmts in_interval (SML)}
    1.24 +  \end{typewriter}
    1.25 +*}
    1.26  
    1.27  text {*
    1.28    \noindent This still is not perfect: the parentheses around the
    1.29 @@ -217,7 +225,11 @@
    1.30  code_const %quotett "op \<and>"
    1.31    (SML infixl 1 "andalso")
    1.32  
    1.33 -text %quote {*@{code_stmts in_interval (SML)}*}
    1.34 +text %quote {*
    1.35 +  \begin{typewriter}
    1.36 +    @{code_stmts in_interval (SML)}
    1.37 +  \end{typewriter}
    1.38 +*}
    1.39  
    1.40  text {*
    1.41    \noindent The attentive reader may ask how we assert that no