Extended ASCII

[Adam Grabowski <adam@math.uwb.edu.pl>]

As far as I know, the Mizar Team continues the work on
porting the Mizar system into Unix platforms. So we
should expect version of the PC Mizar for Linux soon.
(Am I right?)
However, under Unix systems the so-called extended ASCII
used in Mizar articles stored in the Mizar Mathematical
Library may cause even bigger problems than under DOS based.

Introducing of extended ASCII symbols in new vocabularies
is not allowed but many symbols still remain in the MML.

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.
The easy-to-change exceptions are Mizar structure delimiters:
'#174' and '#175' which already have their non-extended-ASCII
equivalents '(#' and '#)', used sometimes by some authors.
I think in this case using of #174 and #175 should be prohibited.

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

Let me describe proposed changes briefly (unfortunately most of
them aren't TeX-inspired):

Format: <character> <character-code> <non-ext.ASCII-proposition>

��  #198#205  |=
�   #195  |-
�Ĵ #195#196#180  |-|
�   #240  <==>
� #243  <= (LATTICE3)
� #253  2 (in METRIC_1 and TOPREAL1)
� #223  -neighbour
� #224  alpha
� #235  delta
� #229  sigma
� #230  mi
� #210  land
� #208  lor
� #158  IncProj
� #236  PProJ or infty
� #157  ProJ
� #179  | (in brackets only with the other characters)
� #171  MidOp or Half
� #159  f
� #174  <
� #175  >
��> #196#196> ===> (PRELAMB)
<��> <#196#196> <===>

(Apologies if your mail browser displays some characters incorrectly, try
our website)

Comments are appreciated.

Greetings
Adam Grabowski
Artur Kornilowicz