Re: Extended ASCII in Mizar

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

Hi:

I support getting rid of the extended ASCII.

However, aside from work needed to do it we should be aware that
it is easy to make a decision as unfortunate as the decision to employ
the extended ASCII.

In the future, there is hope for:

	- using Unicode once it is established,
	- using math symbols in HTML once some standard exists.

In the meantime, any solution will have a temporary character.

But I think it is wortwhile to make the life a bit easier for some people by:

	- defining a standard set of ASCII synonyms for all Mizar tokens
	  and all vocabulary symbols.
	  LaTeX style for these is quite a natural choice, and
	  the "vocabulary committee" should take care of this, one
 	  must not rely on the good will of the contributors if a uniform
	  style is desired.

	  As it is now some vocabulary symbols are awful.

	- immediate prohibition of new vocabulary symbols using extended
	  ASCII characters.

Only if the practice with the new symbols is satisfactory, I would
move to create a revision of MML which does not use any extended ASCII.
Starting the revision right away may cause too much headache.

-- 
Piotr (Peter) Rudnicki