[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:17:08 CET 2016

On Sat, 12 Mar 2016, Florian Haftmann wrote:

>  * All other characters are represented as »Char n«

BTW, these Unicode guillemets cause problems in the NEWS file, which is 
subject to standard Isabelle symbol interpretation. I've changed that in 

Another Unicode accident (by Andreas Lochbihler) is repaired in 
a9ee1f240b81. Luckily we don't rely on raw Unicode under normal 

I usually edit the NEWS file with the "mini-IDE" of Isabelle/jEdit, 
especially the Sidekick view helps to see the structure of this 
increasingly complex file.


More information about the isabelle-dev mailing list