doc-src/Codegen/Thy/Adaptation.thy
changeset 39643 29cc021398fc
parent 39063 5f9692dd621f
child 39664 0afaf89ab591
     1.1 --- a/doc-src/Codegen/Thy/Adaptation.thy	Wed Sep 22 18:40:35 2010 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Adaptation.thy	Thu Sep 23 08:30:33 2010 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4    to introduce inconsistencies -- or, in other words: custom
     1.5    serialisations are completely axiomatic.
     1.6  
     1.7 -  A further noteworthy details is that any special character in a
     1.8 +  A further noteworthy detail is that any special character in a
     1.9    custom serialisation may be quoted using ``@{verbatim "'"}''; thus,
    1.10    in ``@{verbatim "fn '_ => _"}'' the first ``@{verbatim "_"}'' is a
    1.11    proper underscore while the second ``@{verbatim "_"}'' is a
    1.12 @@ -274,13 +274,13 @@
    1.13    For convenience, the default @{text HOL} setup for @{text Haskell}
    1.14    maps the @{class equal} class to its counterpart in @{text Haskell},
    1.15    giving custom serialisations for the class @{class equal} (by command
    1.16 -  @{command_def code_class}) and its operation @{const HOL.equal}
    1.17 +  @{command_def code_class}) and its operation @{const [source] HOL.equal}
    1.18  *}
    1.19  
    1.20  code_class %quotett equal
    1.21    (Haskell "Eq")
    1.22  
    1.23 -code_const %quotett "op ="
    1.24 +code_const %quotett "HOL.equal"
    1.25    (Haskell infixl 4 "==")
    1.26  
    1.27  text {*