[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] New Mizar version (6.3.04_3.50.773)
Hi All,
I'd like to inform you that the new version of Mizar system (6.3.04)
and the Mizar Mathematical Library (3.50.773) is available for all
supported platforms, that is Win32, Linux x86 and Sun Solaris x86.
As it was announced before, we try to build step by step Enyclopedia
of Mathematics in Mizar (EMM). These articles, which MML identifiers
begin with the letter 'X', are collected from the Mizar articles yet
submitted to the MML and authored by Library Committee of the Association
of Mizar Users.
At the very first stage of EMM development we decided to gather
definitions and theorems concerning boolean properties of sets (XBOOLE_0
and XBOOLE_1).
After that we started EMM volumes about numbers - real (XREAL_0) and
complex (XCMPLX_0). Because of the new concept of the definition
of complex numbers (now all objects with the type 'real number'
have also the type 'complex number') introduced in the MML
the 'XCMPLX' series is very important.
The article 'Complex Numbers - Basic Theorems' (XCMPLX_1)
contains 225 theorems, mainly from articles with identifiers
AXIOMS, REAL_1, REAL_2, SEQ_2, SEQ_4, and SQUARE_1.
For your convenience the abstract of XCMPLX_1.ABS is available at
ftp://mizar.uwb.edu.pl/pub/library/
as well as in the above mentioned distribution.
User comments or additional absent theorems are welcome.
Original theorems will be removed from the MML soon. The transition
tables will be announced.
For downloading the whole distro, follow the link on our main page
http://www.mizar.org or http://mizar.uwb.edu.pl
Regards,
Adam Grabowski
Library Committee of the Association of Mizar Users