[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] New Mizar version (6.4.02_3.62.798)
Hi All,
I would like to inform you that the new version of Mizar system (6.4.02)
and the Mizar Mathematical Library (3.62.798) is available for all
supported platforms, that is Win32, Linux x86 and Sun Solaris x86.
Porting to FreeBSD i386 is also considered recently - we need your
feedback.
For those of you intensively using Mizar system this is not new,
Freek Wiedijk reported it some time ago: there is an important restriction
comparing to version 6.3.* or earlier. The ability of reconstruction
of scheme predicates and functions by Mizar verifier is now practically
turned off. Czeslaw Bylinski (and Grzegorz Bancerek) promised to improve
this situation in the future.
As you may have noticed, this caused huge changes of the library
done mainly by hands of the Bialystok team with the help of our
collaborators in Canada and Japan. The practical advice is to introduce
private predicates and functions (using 'defpred' and 'deffunc'
constructions) and to use them in the proofs justified 'from' schemes.
Another substantial change yet noticed by Freek is removing
of unclusterability of attributes. This effected in change of STRUCT_0
article: the definitions of the modes: Element, Subset, Subset-Family
for structures were removed as equal to the ordinary - that of sets.
Further removal of the definitions with 'not contradiction' definiens
is possible. Note also that the complement ` defined for
sets can be used instead of - (again for structures).
Pretty fresh revision is done by Andrzej Trybulec. He made the article
NUMBERS which deals with real numbers. Identifier NUMBERS may be crucial
if you will have any errors concerning ARYTM_0 clusters or notation.
If you encounter any troubles concerning new release, Mizar User
Service (mus@mizar.uwb.edu.pl) can be helpful as usual.
For downloading the whole distribution, 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