NEWS
changeset 62678 843ff6f1de38
parent 62671 a9ee1f240b81
child 62693 0ae225877b68
equal deleted inserted replaced
62677:0df43889f496 62678:843ff6f1de38
    64       are non-canonical.
    64       are non-canonical.
    65   - Printing and parsing:
    65   - Printing and parsing:
    66     * Printable characters are printed and parsed as "CHR ''\<dots>''"
    66     * Printable characters are printed and parsed as "CHR ''\<dots>''"
    67       (as before).
    67       (as before).
    68     * The ASCII zero character is printed and parsed as "0".
    68     * The ASCII zero character is printed and parsed as "0".
    69     * All other canonical characters are printed as "CHAR 0xXX"
    69     * All other canonical characters are printed as "CHR 0xXX"
    70       with XX being the hexadecimal character code.  "CHAR n"
    70       with XX being the hexadecimal character code.  "CHR n"
    71       is parsable for every numeral expression n.
    71       is parsable for every numeral expression n.
    72     * Non-canonical characters have no special syntax and are
    72     * Non-canonical characters have no special syntax and are
    73       printed as their logical representation.
    73       printed as their logical representation.
    74   - Explicit conversions from and to the natural numbers are
    74   - Explicit conversions from and to the natural numbers are
    75     provided as char_of_nat, nat_of_char (as before).
    75     provided as char_of_nat, nat_of_char (as before).