[Date Prev][Date Next] [Chronological] [Thread] [Top]

Extended ASCII



I have the following remarks to the extended ASCII in MML:

-- I don't like the symbol <==> for equivalence of models (ZFREFLE1). I
prefer verbose format "M1, M2 are_equivalent", but
if the exchanging is done automatically, I will accept the verbose synonym.

-- In ZF_COLLA I propose to change the symbol of the functor "M\mu" by
"Collapse"

-- the alpha sign from MONOID_0 should be changed to "otimes" or
"(*)" or "(x)" but the last is dangerous.

-- I strongly support replacing of #242 and #243 with >= and <= in any
symbol.

===============================================================
Grzegorz Bancerek               e-mail: bancerek@mizar.org 
                                        (bancerek@math.uwb.edu.pl)
Dept. of Applied Logic          http://math.uwb.edu.pl/~bancerek/
Institute of Computer Science   fax. +48 (85) 745-7073
University of Bialystok         tel. +48 (85) 745-7559 (office)
15-267 Bialystok, Poland             +48 (85) 719-1984 (home)