src/Doc/Codegen/Adaptation.thy

        String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
        @{typ String.literal}s are mapped to target-language strings.
 
        Literal values of type @{typ String.literal} can be written
        as @{text "STR ''\<dots>''"} for sequences of printable characters and
-       @{text "ASCII 0x\<dots>"} for one single ASCII code point given
+       @{text "STR 0x\<dots>"} for one single ASCII code point given
        as hexadecimal numeral; @{typ String.literal} supports concatenation
        @{text "\<dots> + \<dots>"} for all standard target languages.
 
        Note that the particular notion of \qt{string} is target-language
        specific (sequence of 8-bit units, sequence of unicode code points, \ldots);