'0' replacement

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Recently the team developing Mizar system experimented with internal unifying
the empty set and 0 (numeral). We introduced '0' as a synonym for ALT+237
(the ASCII char currently representing the empty set) in BOOLE and redefined 0
as a real number in ARYTM.
It caused the need to place '0' as a functor identifier in some vocabulary
file. At first we tried to insert it into BOOLE vocabulary, but it doesn't
seem to be the best solution since there is a lot of articles that use
arithmetics and don't require boolean operations. So maybe we should place
it in HIDDEN ? Or maybe some other existing vocabulary, or a new one?
Any comments and suggestions will be appreciated,

Adam Naumowicz