NEWS
changeset 68028 1f9f973eed2a
parent 68027 64559e1ca05b
child 68033 ad4b8b6892c3
     1.1 --- a/NEWS	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/NEWS	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -196,6 +196,36 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Clarified relationship of characters, strings and code generation:
     1.8 +
     1.9 +  * Type "char" is now a proper datatype of 8-bit values.
    1.10 +
    1.11 +  * Conversions "nat_of_char" and "char_of_nat" are gone; use more
    1.12 +    general conversions "of_char" and "char_of" with suitable
    1.13 +    type constraints instead.
    1.14 +
    1.15 +  * The zero character is just written "CHR 0x00", not
    1.16 +    "0" any longer.
    1.17 +
    1.18 +  * Type "String.literal" (for code generation) is now isomorphic
    1.19 +    to lists of 7-bit (ASCII) values; concrete values can be written
    1.20 +    as "STR ''...''" for sequences of printable characters and
    1.21 +    "ASCII 0x..." for one single ASCII code point given
    1.22 +    as hexadecimal numeral.
    1.23 +
    1.24 +  * Type "String.literal" supports concatenation "... + ..."
    1.25 +    for all standard target languages.
    1.26 +
    1.27 +  * Theory Library/Code_Char is gone; study the explanations concerning
    1.28 +    "String.literal" in the tutorial on code generation to get an idea
    1.29 +    how target-language string literals can be converted to HOL string
    1.30 +    values and vice versa.
    1.31 +
    1.32 +  * Imperative-HOL: operation "raise" directly takes a value of type
    1.33 +    "String.literal" as argument, not type "string".
    1.34 +
    1.35 +INCOMPATIBILITY.
    1.36 +
    1.37  * Abstract bit operations as part of Main: push_bit, take_bit,
    1.38  drop_bit.
    1.39