[isabelle-dev] NEWS: Characters (type char) are modelled as finite algebraic type, corresponding to {0..255}

[Makarius]

On Sat, 12 Mar 2016, Florian Haftmann wrote:

> * Simplifying the character syntax further. e.g. getting rid of CHR vs.
>   CHAR.

That should be trivial:

syntax
   "_Char" :: "str_position ⇒ char"  ("CHR _")
   "_Char_ord" :: "num_const ⇒ char"  ("CHR _")


The languages "str_position" and "num_const" are disjoint.


 	Makarius