Re: Extended ASCII

[Freek Wiedijk <freek@cs.kun.nl>]

Dear Piotr,

>Using synonyms you may tailor tokens for vocabulary symbols
>to your liking.

Ah, but is that something that should be encouraged? :-)

One more argument for "in" and "0" over "\in" and "\0": it's
shorter and it is also much easier to type (I always forget
where my bacckslash key is :-))

>Besides, I think that whatever is done in getting rid of
>extended ASCII has a temporary character until Unicode takes
>over (if this happens).

I hope and expect that Unicode will succeed.  Still, even
then I think it would be a good idea to have a "8-bit ascii"
representation of Mizar text, in order to be able to edit it
in old-fashioned editors (like, say, the Turbo Pascal editor,
or like, say, vi.)  Maybe something with, hm, backslashes? :-)

If you want to prepare for Unicode, then "in" should become
something like "\element_of" (or "#element of#"?)  Because
this symbol is Unicode character 0x2208, which has official
Unicode name "ELEMENT OF" (see:
<http://charts.unicode.org/Unicode.charts/normal/U2200.html>.)

Freek