[mizar] EMM Project started

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

  Dear all,
  Library Committee of the Association of Mizar Users decided
to start up Encyclopaedia of Mathematics in Mizar (EMM for short).
It will be closely related to the Mizar Mathematical Library.
  Two first two items are Boolean Properties of Sets - XBOOLE_0
(definitions) and XBOOLE_1 (theorems). The article BOOLE has been
removed so the care is advised with the new version of Mizar
(6.1.10_3.31.718 at the moment).
  XBOOLE_0 contains basic definitions of the empty set, basic
boolean operations (union, meet, difference and symmetric
difference of two sets), attribute 'empty', predicates 'meets',
'misses', 'c<', 'are_c=-comparable' and redefinition of equality
for sets, existential registrations of clusters for empty
and non empty sets and functorial cluster that {} is
empty and three schemes: Separation, Extensionality and SetEq.
  In XBOOLE_1 'boolean' theorems collected from the MML with the
help of MML Query are contained.
  Detailed description of the revision as well as the transition
table from BOOLE into XBOOLE_0 and XBOOLE_1 is under address:
  http://mizar.uwb.edu.pl/library/revisions/rev4.html
  Feel free to contact me or mus@mizar.uwb.edu.pl
if you encounter troubles with verifying your article
under new version of the MML.
  Greetings
  Adam Grabowski
  Library Committee of the Association of Mizar Users