Wishes for Mizar

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Freek Wiedijk has written "Wishes for Mizar":
        www.cs.kun.nl/~freek/mizar/mizarwishes.ps.gz

In it:

"2 Weird characters.
.....
Please only use ASCII characters with codes between 32 and 126."

The decision had been made. The problem is that it is difficult to find out a good
replacement for them.

Recently Adam Grabowski eliminated d237 (empty set). It is replaced by {} (1 word,
not functor brackets).
Actually, a bit more has been done:
 1. synonyms for {}, if they were without arguments have been removed. It is
   <d327> - the empty finite sequence
   empty_rel  - the empty relation (from MARGREL1)
   [] - the empty function
 These synonyms were very useful "before attributes". Now it is not so. E.g.
"Function" is a shortcut for
       "Function-like Relation-like set"
and when conditional registration of clusters is in the environment, then system
knows that the empty set if a function.
Please note that registration of clusters has nothing to do with notation, it is
done on the semantic level.
2. d237 was used also as a part of longer symbols, e.g.
  - <d327>D for the empty set of elements of D, it is a redefinition, then we
still have it, with notation
     <*>D
  - Bancerek's  (MONOID_0)
       D*+^+<d237>
    is replaced by D*+^+<0>

Maybe I have omitted something, just look to the documentation. This part of the
project id, as usual, fully documented and easy accessible.

Also d238 (membership) is replaced by "in". Because of the conflict with the
qualification of the "in" symbol, it had been used in FUNCT_7:def 1 for a functor,
the format in FUNCT_7 is changed. It is now
    In(x,y)
instead of "x in y". So the symbol may be used now for a predicate.

Freek wrote
"I know these characters are already gradually being phased out. I'd prefer to see
this problem in one big substitution operation."

Me, too

Andrzej Trybulec