[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