[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:

> * A type of infinitely many characters could serve a model for unicode
>   characters.

Unicode has only finitely many code points. Presently, 21 bits are 
sufficient to encode that.

Does it make sense to have a char type with somewhat "unspecified" size. 
I.e. one that might change over the years, like Unicode does?


 	Makarius