diff -r bdc1504ad456 -r 03a87478b89e doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu May 14 08:22:07 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu May 14 09:16:33 2009 +0200 @@ -166,7 +166,7 @@ \isa{index} which is mapped to target-language built-in integers. Useful for code setups which involve e.g. indexing of target-language arrays. - \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype + \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{message{\isacharunderscore}string} which is isomorphic to strings; \isa{message{\isacharunderscore}string}s are mapped to target-language strings. Useful for code setups which involve e.g. printing (error) messages.