Re: Extended ASCII

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

Adam Grabowski wrote:


 > I haven't any good idea what to put in place of #237
 > (emptyset seems too long, maybe 0?) or #238 (membership
 > relation - in?). Such a change could be annoying to experienced
 > Mizar users so it should be discussed.

Probably 0 will win but I would like \0 better.
Similarly for #238 my choice would be \in.  I suggest avoiding
short identifiers as vocabulary symbols and prepending them with
a backslash.

 > Firstly I would like to propose some changes to symbols
 > which are used not so often. The propositions are collected
 > on the Mizar Website:
 > 
 > http://mizar.org/library/preds.html

A side remark: Recently, I find connecting to mizar.org very slow and
               unreliable.  Connections to http://mizar.uwb.edu.pl are
               much faster.

Some comments about the proposed changes:

 > ð   #240  <==>

<=> seems shorter.

 > ý #253  2 (in METRIC_1 and TOPREAL1)

How about ^2?

 > à #224  alpha
 > ë #235  delta
 > å #229  sigma
 > æ #230  mi

All Greek letters can be written with a Latin letter prepended with \.
So alpha would be \a.

 > ÄÄ> #196#196> ===> (PRELAMB)
 > <ÄÄ> <#196#196> <===>

These are a bit long and 'thick', unfortunately, --> and ==> are used
as symbols of operations.

When Andrzej was in Edmonton during the summer, in an article about
reduction rings (not finished) we introduced symbols for a one step
reduction 

	==>.

and a transitively closed reduction

	==>*

(With <==>. and <==>* for two directional reductions.)

May be these symbols can be used instead of what is proposed for the symbols
from PRELAMB.

Are there any suggestions for extended-ASCII symbols from HIDDEN?

Cheers,

Piotr Rudnicki