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

Makarius makarius at sketis.net
Sat Mar 19 11:26:38 CET 2016

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:

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

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


More information about the isabelle-dev mailing list