doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy
changeset 28447 df77ed974a78
parent 28428 fd007794561f
child 28456 7a558c872104
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Wed Oct 01 12:18:18 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Adaption.thy	Wed Oct 01 13:33:54 2008 +0200
     1.3 @@ -66,12 +66,12 @@
     1.4  
     1.5  primrec %quoteme in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
     1.6    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
     1.7 -
     1.8 +(*<*)
     1.9  code_type %invisible bool
    1.10    (SML)
    1.11  code_const %invisible True and False and "op \<and>" and Not
    1.12    (SML and and and)
    1.13 -
    1.14 +(*>*)
    1.15  text %quoteme {*@{code_stmts in_interval (SML)}*}
    1.16  
    1.17  text {*
    1.18 @@ -92,7 +92,7 @@
    1.19    (SML "true" and "false" and "_ andalso _")
    1.20  
    1.21  text {*
    1.22 -  The @{command code_type} command takes a type constructor
    1.23 +  \noindent The @{command code_type} command takes a type constructor
    1.24    as arguments together with a list of custom serialisations.
    1.25    Each custom serialisation starts with a target language
    1.26    identifier followed by an expression, which during
    1.27 @@ -120,22 +120,22 @@
    1.28  text %quoteme {*@{code_stmts in_interval (SML)}*}
    1.29  
    1.30  text {*
    1.31 -  Next, we try to map HOL pairs to SML pairs, using the
    1.32 +  \noindent Next, we try to map HOL pairs to SML pairs, using the
    1.33    infix ``@{verbatim "*"}'' type constructor and parentheses:
    1.34  *}
    1.35 -
    1.36 +(*<*)
    1.37  code_type %invisible *
    1.38    (SML)
    1.39  code_const %invisible Pair
    1.40    (SML)
    1.41 -
    1.42 +(*>*)
    1.43  code_type %tt *
    1.44    (SML infix 2 "*")
    1.45  code_const %tt Pair
    1.46    (SML "!((_),/ (_))")
    1.47  
    1.48  text {*
    1.49 -  The initial bang ``@{verbatim "!"}'' tells the serializer to never put
    1.50 +  \noindent The initial bang ``@{verbatim "!"}'' tells the serializer to never put
    1.51    parentheses around the whole expression (they are already present),
    1.52    while the parentheses around argument place holders
    1.53    tell not to put parentheses around the arguments.
    1.54 @@ -178,7 +178,7 @@
    1.55    (Haskell infixl 4 "==")
    1.56  
    1.57  text {*
    1.58 -  A problem now occurs whenever a type which
    1.59 +  \noindent A problem now occurs whenever a type which
    1.60    is an instance of @{class eq} in @{text HOL} is mapped
    1.61    on a @{text Haskell}-built-in type which is also an instance
    1.62    of @{text Haskell} @{text Eq}:
    1.63 @@ -199,7 +199,7 @@
    1.64    (Haskell "Integer")
    1.65  
    1.66  text {*
    1.67 -  The code generator would produce
    1.68 +  \noindent The code generator would produce
    1.69    an additional instance, which of course is rejectedby the @{text Haskell}
    1.70    compiler.
    1.71    To suppress this additional instance, use