Extended ASCII

[Library Committee <mml@mizar.uwb.edu.pl>]

Below you will find the propositions for the revision
of the Mizar Mathematical Library. The aim is to remove
all extended ASCII characters from Mizar articles.
As of now, only 19 left in 15 vocabularies.

In the text below extended ASCII characters are encoded
according to
    http://mizar.org/JFM/ASCII/ExtAscii.html
    ('#'<decimal_number>)

Vocabulary BOOLE:
Current_form    Proposition_of_replacement
U               \/
#239            /\
#246            /+/

Vocabulary LATTICES:
#193            Bottom
#194            Top

Vocabulary FINITER2:
#166            [;]
#167            [:]

Vocabulary FUNC_REL:
#248            .:

Vocabulary CAT3:
[#249]          [*]

Vocabulary MSUALG_3:
#248#248        .:.:
#249#249        **

Vocabulary HIDDEN:
#249            *

Vocabulary MULTISET:
#248^2          .:^2

Vocabulary PI:
#227            pi

Vocabulary SIGMA:
#228            Sum

Vocabulary SUB_OP:
#234            #

Vocabulary NATTRANS:
#250            `*`

Vocabulary SEQ1:
#254            [*]

Vocabulary WELLORD:
|#253           |_2

Vocabulary NAT_1:
#179            divides

Comments are welcome.

Adam Grabowski

------------

Library Committee of the Association of Mizar Users