[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 
a2351f82bc48.

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


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.


 	Makarius


More information about the isabelle-dev mailing list